JBMC example with data structures

[shankarapailoor]

JBMC/CBMC version: 5.8
Operating system: Linux 5.0
What behaviour did you expect: An assertion failure
What happened instead: JBMC reports success

Hi,

I'm testing out JBMC and I want to see if it can verify some assertions over data structures and I gave the following simple example:

package my.petty.examples;
import java.util.HashMap;
import java.util.Map;
import java.util.Set;
import java.util.HashSet;
import java.util.List;
import java.util.LinkedList;

public class Simple {
	public static Map<String, Integer> name2score;
	public static Set<String> names;

	public static boolean validate() {
		for (Map.Entry<String, Integer> entry : name2score.entrySet()) {
			String key = entry.getKey();
			if (!names.contains(key))
				return false;
		}
		if (names.size() != name2score.size())
			return false;
		return true;
	}

	public static void main(String[] args) {
		name2score = new HashMap<String, Integer>();
		names = new HashSet<String>();
		name2score.put("Shankara", 20);
		names.add("Shankar");
		System.out.println(validate()); //false
		assert(validate()); //jbmc doesn't report failure
	}
}

The full command I used to run JBMC was

~/cbmc-jbmc-5.8-cav18/src/jbmc/jbmc --z3 my/petty/examples/Simple.class --unwind 10 --classpath ~/cbmc-jbmc-5.8-cav18/src/java_bytecode/library/core-models.jar:.

Do these data structures need to be added to the JOM?