mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

fixing compilation errors

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-05-03 03:18:29 -07:00
parent bb041495e3
commit e98c808f47
2 changed files with 2 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
examples/dotnet/Program.cs
View file

@ -611,7 +611,6 @@ namespace test_mapi
Expr f_x = ctx.MkApp(f, x); Expr f_x = ctx.MkApp(f, x);
Expr f_y = ctx.MkApp(f, y); Expr f_y = ctx.MkApp(f, y);
Expr g_y = ctx.MkApp(g, y); Expr g_y = ctx.MkApp(g, y);
Pattern[] pats = new Pattern[] { ctx.MkPattern(new Expr[] { f_x, g_y }) };
Expr[] no_pats = new Expr[] { f_y }; Expr[] no_pats = new Expr[] { f_y };
Expr[] bound = new Expr[2] { x, y }; Expr[] bound = new Expr[2] { x, y };
Expr body = ctx.MkAnd(ctx.MkEq(f_x, f_y), ctx.MkEq(f_y, g_y)); Expr body = ctx.MkAnd(ctx.MkEq(f_x, f_y), ctx.MkEq(f_y, g_y));
@ -628,7 +627,6 @@ namespace test_mapi
Expr f_x = ctx.MkApp(f, x); Expr f_x = ctx.MkApp(f, x);
Expr f_y = ctx.MkApp(f, y); Expr f_y = ctx.MkApp(f, y);
Expr g_y = ctx.MkApp(g, y); Expr g_y = ctx.MkApp(g, y);
Pattern[] pats = new Pattern[] { ctx.MkPattern(new Expr[] { f_x, g_y }) };
Expr[] no_pats = new Expr[] { f_y }; Expr[] no_pats = new Expr[] { f_y };
Symbol[] names = new Symbol[] { ctx.MkSymbol("x"), ctx.MkSymbol("y") }; Symbol[] names = new Symbol[] { ctx.MkSymbol("x"), ctx.MkSymbol("y") };
Sort[] sorts = new Sort[] { ctx.IntSort, ctx.IntSort }; Sort[] sorts = new Sort[] { ctx.IntSort, ctx.IntSort };
@ -729,7 +727,6 @@ namespace test_mapi
{ {
Console.WriteLine("BasicTests"); Console.WriteLine("BasicTests");
Symbol qi = ctx.MkSymbol(1);
Symbol fname = ctx.MkSymbol("f"); Symbol fname = ctx.MkSymbol("f");
Symbol x = ctx.MkSymbol("x"); Symbol x = ctx.MkSymbol("x");
Symbol y = ctx.MkSymbol("y"); Symbol y = ctx.MkSymbol("y");
@ -1319,7 +1316,7 @@ namespace test_mapi
new Sort[] { int_type, int_type } // types of projection operators new Sort[] { int_type, int_type } // types of projection operators
); );
FuncDecl first = tuple.FieldDecls[0]; // declarations are for projections FuncDecl first = tuple.FieldDecls[0]; // declarations are for projections
FuncDecl second = tuple.FieldDecls[1]; // FuncDecl second = tuple.FieldDecls[1];
Expr x = ctx.MkConst("x", int_type); Expr x = ctx.MkConst("x", int_type);
Expr y = ctx.MkConst("y", int_type); Expr y = ctx.MkConst("y", int_type);
Expr n1 = tuple.MkDecl[x, y]; Expr n1 = tuple.MkDecl[x, y];

2
examples/java/JavaExample.java
View file

@ -1508,7 +1508,7 @@ class JavaExample
* parenthesis * parenthesis
*/ */
"(declare-const x Int (declare-const y Int)) (assert (> x y))", "(declare-const x Int (declare-const y Int)) (assert (> x y))",
null, null, null, null)[0]; null, null, null, null);
} catch (Z3Exception e) } catch (Z3Exception e)
{ {
System.out.println("Z3 error: " + e); System.out.println("Z3 error: " + e);