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

deal with ambiguity

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-04 19:12:51 +05:30
parent 5f8c97532c
commit 60af4a5820
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
examples/dotnet/Program.cs
View file

@ -1945,7 +1945,7 @@ namespace test_mapi
BoolExpr p2 = ctx.MkBoolConst("P2"); BoolExpr p2 = ctx.MkBoolConst("P2");
BoolExpr p3 = ctx.MkBoolConst("P3"); BoolExpr p3 = ctx.MkBoolConst("P3");
BoolExpr p4 = ctx.MkBoolConst("P4"); BoolExpr p4 = ctx.MkBoolConst("P4");
BoolExpr[] assumptions = new BoolExpr[] { ctx.MkNot(p1), ctx.MkNot(p2), ctx.MkNot(p3), ctx.MkNot(p4) }; Expr[] assumptions = new Expr[] { ctx.MkNot(p1), ctx.MkNot(p2), ctx.MkNot(p3), ctx.MkNot(p4) };
BoolExpr f1 = ctx.MkAnd(new BoolExpr[] { pa, pb, pc }); BoolExpr f1 = ctx.MkAnd(new BoolExpr[] { pa, pb, pc });
BoolExpr f2 = ctx.MkAnd(new BoolExpr[] { pa, ctx.MkNot(pb), pc }); BoolExpr f2 = ctx.MkAnd(new BoolExpr[] { pa, ctx.MkNot(pb), pc });
BoolExpr f3 = ctx.MkOr(ctx.MkNot(pa), ctx.MkNot(pc)); BoolExpr f3 = ctx.MkOr(ctx.MkNot(pa), ctx.MkNot(pc));