I'm trying to use new Java API from unstable branch in my research project.
I've built jar library from source on Windows 64 bit by folowing instructions in Leonardo de Moura's blog here
The folowing example demonstrate different results of using Java API methods:
1) In the first example I try to fill the Solver with BoolExpr manually using solver.Assert() method
2) In the second example I read the SMT file and parse it's contents with context.ParseSMTLIB2File() method
The expected result of running these examples is UNSATISFIABLE, but first example result is SATISFIABLE and second is UNSATISFIABLE.
All the expressions in both cases are the same, but statistics of the solvers is different.
It seems that in the first example Z3 does not instantiate quantifier properly.