#404 Can't statically check files with HashMaps

[Dr Ian Bayley]

With the file (not very useful as I made it as small as possible to show the error)
class C {
private java.util.Hashtable<string,string> m;
}</string,string>

The command
C:\Users\p0074564\Desktop\JML>java -jar openjml.jar -esc -prover z3_4_3 -exec C:
\Users\p0074564\Desktop\z3-4.3.0-x64\z3-4.3.0-x64\bin\z3.exe -noPurityCheck C.java

Gives the output
Picked up JAVA_TOOL_OPTIONS: -Djava.vendor="Sun Microsystems Inc."
error: An error while executing a proof script for <init>: (error "line 35 colum
n 49: unexpected character")
1 error</init>

There is no such problem with ArrayList. Perhaps HashMap has not been implemented yet?

[David Cok]

The problem appears to be with HashMap and its use of floating point, and that the Z3 solver takes a very long time on floating point problems.