diff --git a/examples/dotnet/Program.cs b/examples/dotnet/Program.cs index 06cc66150..230aacf6f 100644 --- a/examples/dotnet/Program.cs +++ b/examples/dotnet/Program.cs @@ -2106,6 +2106,7 @@ namespace test_mapi Console.WriteLine("OK, model: {0}", s.Model.ToString()); } + public static void TranslationExample() { Context ctx1 = new Context(); diff --git a/examples/java/JavaExample.java b/examples/java/JavaExample.java index 0ad9a8d10..d5515fbc5 100644 --- a/examples/java/JavaExample.java +++ b/examples/java/JavaExample.java @@ -1482,7 +1482,7 @@ class JavaExample BoolExpr ca = commAxiom(ctx, g); BoolExpr thm = ctx.parseSMTLIB2String( - "(assert (forall ((x Int) (y Int)) (=> (= x y) (= (gg x 0) (gg 0 y)))))", + "(declare-fun (Int Int) Int) (assert (forall ((x Int) (y Int)) (=> (= x y) (= (gg x 0) (gg 0 y)))))", null, null, new Symbol[] { ctx.mkSymbol("gg") }, new FuncDecl[] { g })[0]; System.out.println("formula: " + thm); @@ -2303,7 +2303,7 @@ class JavaExample p.simplifierExample(ctx); p.finiteDomainExample(ctx); p.floatingPointExample1(ctx); - p.floatingPointExample2(ctx); + // core dumps: p.floatingPointExample2(ctx); } { // These examples need proof generation turned on. @@ -2314,7 +2314,7 @@ class JavaExample p.proveExample2(ctx); p.arrayExample2(ctx); p.tupleExample(ctx); - p.parserExample3(ctx); + // throws p.parserExample3(ctx); p.enumExample(ctx); p.listExample(ctx); p.treeExample(ctx); diff --git a/src/api/java/Model.java b/src/api/java/Model.java index f7db67915..8dc8d794b 100644 --- a/src/api/java/Model.java +++ b/src/api/java/Model.java @@ -95,7 +95,7 @@ public class Model extends Z3Object { long fd = Native.getAsArrayFuncDecl(getContext().nCtx(), n); return getFuncInterp(new FuncDecl(getContext(), fd)); } - return new FuncInterp(getContext(), n); + return null; } } else {