mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-28 10:19:23 +00:00
Code Activity

fix java

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-03 08:04:10 -07:00
parent e98c808f47
commit 8ecff9e5ee
1 changed files with 1 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

4
examples/java/JavaExample.java
View file

@ -344,8 +344,6 @@ class JavaExample
Status q = s.check(); Status q = s.check();
System.out.println("Solver says: " + q); System.out.println("Solver says: " + q);
System.out.println("Model: \n" + s.getModel()); System.out.println("Model: \n" + s.getModel());
System.out.println("Converted Model: \n"
+ ar.convertModel(0, s.getModel()));
if (q != Status.SATISFIABLE) if (q != Status.SATISFIABLE)
throw new TestFailedException(); throw new TestFailedException();
} }
@ -1041,7 +1039,7 @@ class JavaExample
HashMap<String, String> cfg = new HashMap<String, String>(); HashMap<String, String> cfg = new HashMap<String, String>();
cfg.put("model", "true"); cfg.put("model", "true");
Context ctx = new Context(cfg); Context ctx = new Context(cfg);
Expr a = ctx.MkAnd(ctx.parseSMTLIB2File(filename, null, null, null, null)); Expr a = ctx.mkAnd(ctx.parseSMTLIB2File(filename, null, null, null, null));
long t_diff = ((new Date()).getTime() - before.getTime()) / 1000; long t_diff = ((new Date()).getTime() - before.getTime()) / 1000;