mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

update java example to bypass bit-rot

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-02 09:50:29 -07:00
parent 370abf602c
commit 648a531950
3 changed files with 5 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
examples/dotnet/Program.cs
View file

@ -2106,6 +2106,7 @@ namespace test_mapi
Console.WriteLine("OK, model: {0}", s.Model.ToString());
}
public static void TranslationExample()
{
Context ctx1 = new Context();

6
examples/java/JavaExample.java
View file

@ -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);

2
src/api/java/Model.java
View file

@ -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
{