From bb041495e39f8e7ac384554962168c355c3c288a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 2 May 2018 14:00:37 -0700
Subject: [PATCH] fix java

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/java/JavaExample.java | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java
index 7b8902768..90460de05 100644
--- a/examples/java/JavaExample.java
+++ b/examples/java/JavaExample.java
@@ -167,12 +167,12 @@ class JavaExample
                     "function must be binary, and argument types must be equal to return type");
         }
 
-        String bench = "(benchmark comm :formula (forall (x " + t.getName()
+        String bench = "(assert (forall (x " + t.getName()
                 + ") (y " + t.getName() + ") (= (" + f.getName() + " x y) ("
                 + f.getName() + " y x))))";
         return ctx.parseSMTLIB2String(bench, new Symbol[] { t.getName() },
                 new Sort[] { t }, new Symbol[] { f.getName() },
-                new FuncDecl[] { f });
+                new FuncDecl[] { f })[0];
     }
 
     // / "Hello world" example: create a Z3 logical context, and delete it.
@@ -1041,7 +1041,7 @@ class JavaExample
             HashMap<String, String> cfg = new HashMap<String, String>();
             cfg.put("model", "true");
             Context ctx = new Context(cfg);
-            Expr a = 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;
 
@@ -1445,7 +1445,7 @@ class JavaExample
 
         BoolExpr f = ctx.parseSMTLIB2String(
                 "(declare-const x Int) (declare-const y Int) (assert (and (> x y) (> x 0)))",
-                null, null, null, null);
+                null, null, null, null)[0];
         System.out.println("formula " + f);
 
         @SuppressWarnings("unused")
@@ -1465,7 +1465,7 @@ class JavaExample
         FuncDecl[] decls = new FuncDecl[] { a, b };
 
         BoolExpr f = ctx.parseSMTLIB2String("(assert (> a b))", null, null,
-                declNames, decls);
+                declNames, decls)[0];
         System.out.println("formula: " + f);
         check(ctx, f, Status.SATISFIABLE);
     }
@@ -1486,7 +1486,7 @@ class JavaExample
         BoolExpr thm = ctx.parseSMTLIB2String(
                 "(assert (forall ((x Int) (y Int)) (=> (= x y) (= (gg x 0) (gg 0 y)))))",
                 null, null, new Symbol[] { ctx.mkSymbol("gg") },
-                new FuncDecl[] { g });
+                new FuncDecl[] { g })[0];
         System.out.println("formula: " + thm);
         prove(ctx, thm, false, ca);
     }
@@ -1508,7 +1508,7 @@ class JavaExample
                      * parenthesis
                      */
                     "(declare-const x Int (declare-const y Int)) (assert (> x y))",
-                    null, null, null, null);
+                    null, null, null, null)[0];
         } catch (Z3Exception e)
         {
             System.out.println("Z3 error: " + e);