summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Test/alltests.txt1
-rw-r--r--Test/prover/Answer50
-rw-r--r--Test/prover/EQ_v2.Eval__v4.Eval_out.bpl2255
-rw-r--r--Test/prover/runtest.bat13
-rw-r--r--Test/prover/z3mutl.bpl22
5 files changed, 2341 insertions, 0 deletions
diff --git a/Test/alltests.txt b/Test/alltests.txt
index 48f132de..b2d093cc 100644
--- a/Test/alltests.txt
+++ b/Test/alltests.txt
@@ -17,6 +17,7 @@ bitvectors Use Smoke tests for bitvectors
smoke Use Soundness smoke testing
test16 Use Tests loop unrolling
codeexpr Use Tests code expressions
+prover Use Tests checking various prover options
test17 Postponed Tests inference of parameterized contracts
z3api Postponed Test for Z3 Managed .NET API prover
houdini Postponed Test for Houdini decision procedure
diff --git a/Test/prover/Answer b/Test/prover/Answer
new file mode 100644
index 00000000..1ca6407c
--- /dev/null
+++ b/Test/prover/Answer
@@ -0,0 +1,50 @@
+==================== -z3multipleErrors ========================
+
+-------------------- z3mutl.bpl --------------------
+z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ z3mutl.bpl(5,1): start
+ z3mutl.bpl(14,1): L3
+ z3mutl.bpl(20,1): L5
+z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ z3mutl.bpl(5,1): start
+ z3mutl.bpl(11,1): L2
+ z3mutl.bpl(20,1): L5
+z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.
+Execution trace:
+ z3mutl.bpl(5,1): start
+ z3mutl.bpl(8,1): L1
+ z3mutl.bpl(20,1): L5
+
+Boogie program verifier finished with 0 verified, 3 errors
+
+-------------------- EQ_v2.Eval__v4.Eval_out.bpl --------------------
+EQ_v2.Eval__v4.Eval_out.bpl(2101,5): Error BP5003: A postcondition might not hold on this return path.
+EQ_v2.Eval__v4.Eval_out.bpl(1715,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ EQ_v2.Eval__v4.Eval_out.bpl(1786,3): AA_INSTR_EQ_BODY
+ EQ_v2.Eval__v4.Eval_out.bpl(1862,3): inline$v2.Eval$0$label_11_case_2#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1894,3): inline$v2.Eval$0$label_12#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1989,3): inline$v4.Eval$0$label_11_case_2#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2011,3): inline$v4.Eval$0$label_14_true#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2081,3): inline$v4.Eval$0$label_12#2
+EQ_v2.Eval__v4.Eval_out.bpl(2101,5): Error BP5003: A postcondition might not hold on this return path.
+EQ_v2.Eval__v4.Eval_out.bpl(1715,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ EQ_v2.Eval__v4.Eval_out.bpl(1786,3): AA_INSTR_EQ_BODY
+ EQ_v2.Eval__v4.Eval_out.bpl(1875,3): inline$v2.Eval$0$label_11_case_1#2
+ EQ_v2.Eval__v4.Eval_out.bpl(1894,3): inline$v2.Eval$0$label_12#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2032,3): inline$v4.Eval$0$label_11_case_1#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2054,3): inline$v4.Eval$0$label_13_true#2
+ EQ_v2.Eval__v4.Eval_out.bpl(2081,3): inline$v4.Eval$0$label_12#2
+EQ_v2.Eval__v4.Eval_out.bpl(2152,5): Error BP5003: A postcondition might not hold on this return path.
+EQ_v2.Eval__v4.Eval_out.bpl(2120,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ EQ_v2.Eval__v4.Eval_out.bpl(2133,3): AA_INSTR_EQ_BODY
+EQ_v2.Eval__v4.Eval_out.bpl(2192,5): Error BP5003: A postcondition might not hold on this return path.
+EQ_v2.Eval__v4.Eval_out.bpl(2167,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+ EQ_v2.Eval__v4.Eval_out.bpl(2178,3): AA_INSTR_EQ_BODY
+
+Boogie program verifier finished with 6 verified, 4 errors
diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
new file mode 100644
index 00000000..e4da94f4
--- /dev/null
+++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
@@ -0,0 +1,2255 @@
+var v4.Mem: [name][int]int;
+
+var v4.alloc: int;
+
+var v4.Mem_T.INT4: [int]int;
+
+var v4.Mem_T.op1__EXPR: [int]int;
+
+var v4.Mem_T.op2__EXPR: [int]int;
+
+var v4.Mem_T.oper__EXPR: [int]int;
+
+var v4.Mem_T.result__EXPR: [int]int;
+
+var v4.detChoiceCnt: int;
+
+var v4.Res_KERNEL_SOURCE: [int]int;
+
+var v4.Res_PROBED: [int]int;
+
+var v4.isUnsigned: int;
+
+const unique v4.T.oper__EXPR: name;
+
+const unique v4.T.op1__EXPR: name;
+
+const unique v4.T.op2__EXPR: name;
+
+const unique v4.T.result__EXPR: name;
+
+const unique v4.T.INT4: name;
+
+const unique v4.T.PINT4: name;
+
+const unique v4.T.PPINT4: name;
+
+const unique v4.T.PP_EXPR: name;
+
+const unique v4.T.P_EXPR: name;
+
+const unique v4.T._EXPR: name;
+
+const {:model_const "e->op2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 23} unique v4.__ctobpl_const_9: int;
+
+const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 24} unique v4.__ctobpl_const_10: int;
+
+const {:model_const "op"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 26} unique v4.__ctobpl_const_11: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 41} unique v4.__ctobpl_const_12: int;
+
+const {:model_const "e->op1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 22} unique v4.__ctobpl_const_6: int;
+
+const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 23} unique v4.__ctobpl_const_7: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 23} unique v4.__ctobpl_const_8: int;
+
+const {:model_const "e->oper"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 21} unique v4.__ctobpl_const_3: int;
+
+const {:model_const "op"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 21} unique v4.__ctobpl_const_1: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 21} unique v4.__ctobpl_const_2: int;
+
+const {:model_const "e->result"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 41} unique v4.__ctobpl_const_13: int;
+
+const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 41} unique v4.__ctobpl_const_14: int;
+
+const {:model_const "isUnsigned"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 29} unique v4.__ctobpl_const_15: int;
+
+const {:model_const "isUnsigned"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 35} unique v4.__ctobpl_const_16: int;
+
+const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 38} unique v4.__ctobpl_const_17: int;
+
+const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 38} unique v4.__ctobpl_const_18: int;
+
+const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 38} unique v4.__ctobpl_const_19: int;
+
+const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_20: int;
+
+const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_21: int;
+
+const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_22: int;
+
+const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_23: int;
+
+const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_24: int;
+
+const {:model_const "result.UnsignedSub"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 36} unique v4.__ctobpl_const_25: int;
+
+const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 32} unique v4.__ctobpl_const_26: int;
+
+const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 32} unique v4.__ctobpl_const_27: int;
+
+const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 32} unique v4.__ctobpl_const_28: int;
+
+const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_29: int;
+
+const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_30: int;
+
+const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_31: int;
+
+const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_32: int;
+
+const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_33: int;
+
+const {:model_const "result.UnsignedAdd"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 30} unique v4.__ctobpl_const_34: int;
+
+const {:model_const "isUnsigned"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 47} unique v4.__ctobpl_const_35: int;
+
+const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 22} unique v4.__ctobpl_const_4: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 22} unique v4.__ctobpl_const_5: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 48} unique v4.__ctobpl_const_36: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 48} unique v4.__ctobpl_const_37: int;
+
+const {:model_const "outval"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 49} unique v4.__ctobpl_const_38: int;
+
+const {:model_const "*outval"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 49} unique v4.__ctobpl_const_39: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 49} unique v4.__ctobpl_const_40: int;
+
+const {:model_const "e->result"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 49} unique v4.__ctobpl_const_41: int;
+
+const {:model_const "isUnsigned"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 54} unique v4.__ctobpl_const_42: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 55} unique v4.__ctobpl_const_43: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceLine 55} unique v4.__ctobpl_const_44: int;
+
+function v4.OneByteToInt(arg_0: byte) : int;
+
+function v4.TwoBytesToInt(arg_0: byte, arg_1: byte) : int;
+
+function v4.FourBytesToInt(arg_0: byte, arg_1: byte, arg_2: byte, arg_3: byte) : int;
+
+function v4.Field(arg_0: int) : name;
+
+function v4.Base(arg_0: int) : int;
+
+function v4.Match(a: int, t: name) : bool;
+
+function v4.MatchBase(b: int, a: int, t: name) : bool;
+
+function v4.HasType(v: int, t: name) : bool;
+
+function v4.T.Ptr(t: name) : name;
+
+function v4.op1__EXPR(arg_0: int) : int;
+
+function v4.op1__EXPRInv(arg_0: int) : int;
+
+function v4._S_op1__EXPR(arg_0: [int]bool) : [int]bool;
+
+function v4._S_op1__EXPRInv(arg_0: [int]bool) : [int]bool;
+
+function v4.op2__EXPR(arg_0: int) : int;
+
+function v4.op2__EXPRInv(arg_0: int) : int;
+
+function v4._S_op2__EXPR(arg_0: [int]bool) : [int]bool;
+
+function v4._S_op2__EXPRInv(arg_0: [int]bool) : [int]bool;
+
+function v4.oper__EXPR(arg_0: int) : int;
+
+function v4.oper__EXPRInv(arg_0: int) : int;
+
+function v4._S_oper__EXPR(arg_0: [int]bool) : [int]bool;
+
+function v4._S_oper__EXPRInv(arg_0: [int]bool) : [int]bool;
+
+function v4.result__EXPR(arg_0: int) : int;
+
+function v4.result__EXPRInv(arg_0: int) : int;
+
+function v4._S_result__EXPR(arg_0: [int]bool) : [int]bool;
+
+function v4._S_result__EXPRInv(arg_0: [int]bool) : [int]bool;
+
+function v4.INT_EQ(x: int, y: int) : bool;
+
+function v4.INT_NEQ(x: int, y: int) : bool;
+
+function v4.INT_ADD(x: int, y: int) : int;
+
+function v4.INT_SUB(x: int, y: int) : int;
+
+function v4.INT_MULT(x: int, y: int) : int;
+
+function v4.INT_DIV(x: int, y: int) : int;
+
+function v4.INT_LT(x: int, y: int) : bool;
+
+function v4.INT_ULT(x: int, y: int) : bool;
+
+function v4.INT_LEQ(x: int, y: int) : bool;
+
+function v4.INT_ULEQ(x: int, y: int) : bool;
+
+function v4.INT_GT(x: int, y: int) : bool;
+
+function v4.INT_UGT(x: int, y: int) : bool;
+
+function v4.INT_GEQ(x: int, y: int) : bool;
+
+function v4.INT_UGEQ(x: int, y: int) : bool;
+
+function v4.BV32_EQ(x: bv32, y: bv32) : bool;
+
+function v4.BV32_NEQ(x: bv32, y: bv32) : bool;
+
+function {:bvbuiltin "bvadd"} v4.BV32_ADD(x: bv32, y: bv32) : bv32;
+
+function {:bvbuiltin "bvsub"} v4.BV32_SUB(x: bv32, y: bv32) : bv32;
+
+function {:bvbuiltin "bvmul"} v4.BV32_MULT(x: bv32, y: bv32) : bv32;
+
+function {:bvbuiltin "bvudiv"} v4.BV32_DIV(x: bv32, y: bv32) : bv32;
+
+function {:bvbuiltin "bvult"} v4.BV32_ULT(x: bv32, y: bv32) : bool;
+
+function {:bvbuiltin "bvslt"} v4.BV32_LT(x: bv32, y: bv32) : bool;
+
+function {:bvbuiltin "bvule"} v4.BV32_ULEQ(x: bv32, y: bv32) : bool;
+
+function {:bvbuiltin "bvsle"} v4.BV32_LEQ(x: bv32, y: bv32) : bool;
+
+function {:bvbuiltin "bvugt"} v4.BV32_UGT(x: bv32, y: bv32) : bool;
+
+function {:bvbuiltin "bvsgt"} v4.BV32_GT(x: bv32, y: bv32) : bool;
+
+function {:bvbuiltin "bvuge"} v4.BV32_UGEQ(x: bv32, y: bv32) : bool;
+
+function {:bvbuiltin "bvsge"} v4.BV32_GEQ(x: bv32, y: bv32) : bool;
+
+function v4.MINUS_BOTH_PTR_OR_BOTH_INT(a: int, b: int, size: int) : int;
+
+function v4.MINUS_LEFT_PTR(a: int, a_size: int, b: int) : int;
+
+function v4.PLUS(a: int, a_size: int, b: int) : int;
+
+function v4.MULT(a: int, b: int) : int;
+
+function v4.DIV(a: int, b: int) : int;
+
+function v4.BINARY_BOTH_INT(a: int, b: int) : int;
+
+function v4.POW2(a: int) : bool;
+
+function v4.BIT_BAND(a: int, b: int) : int;
+
+function v4.BIT_BOR(a: int, b: int) : int;
+
+function v4.BIT_BXOR(a: int, b: int) : int;
+
+function v4.BIT_BNOT(a: int) : int;
+
+function v4.choose(a: bool, b: int, c: int) : int;
+
+function v4.LIFT(a: bool) : int;
+
+function v4.PTR_NOT(a: int) : int;
+
+function v4.NULL_CHECK(a: int) : int;
+
+function v4.NewAlloc(x: int, y: int) : int;
+
+function v4.DetChoiceFunc(a: int) : int;
+
+function v4.Equal(arg_0: [int]bool, arg_1: [int]bool) : bool;
+
+function v4.Subset(arg_0: [int]bool, arg_1: [int]bool) : bool;
+
+function v4.Disjoint(arg_0: [int]bool, arg_1: [int]bool) : bool;
+
+function v4.Empty() : [int]bool;
+
+function v4.SetTrue() : [int]bool;
+
+function v4.Singleton(arg_0: int) : [int]bool;
+
+function v4.Reachable(arg_0: [int,int]bool, arg_1: int) : [int]bool;
+
+function v4.Union(arg_0: [int]bool, arg_1: [int]bool) : [int]bool;
+
+function v4.Intersection(arg_0: [int]bool, arg_1: [int]bool) : [int]bool;
+
+function v4.Difference(arg_0: [int]bool, arg_1: [int]bool) : [int]bool;
+
+function v4.Dereference(arg_0: [int]bool, arg_1: [int]int) : [int]bool;
+
+function v4.Inverse(f: [int]int, x: int) : [int]bool;
+
+function v4.AtLeast(arg_0: int, arg_1: int) : [int]bool;
+
+function v4.Rep(arg_0: int, arg_1: int) : int;
+
+function v4.Array(arg_0: int, arg_1: int, arg_2: int) : [int]bool;
+
+function v4.Unified(arg_0: [name][int]int) : [int]int;
+
+function v4.value_is(c: int, e: int) : bool;
+
+axiom (forall b0: byte, c0: byte :: { v4.OneByteToInt(b0), v4.OneByteToInt(c0) } v4.OneByteToInt(b0) == v4.OneByteToInt(c0) ==> b0 == c0);
+
+axiom (forall b0: byte, b1: byte, c0: byte, c1: byte :: { v4.TwoBytesToInt(b0, b1), v4.TwoBytesToInt(c0, c1) } v4.TwoBytesToInt(b0, b1) == v4.TwoBytesToInt(c0, c1) ==> b0 == c0 && b1 == c1);
+
+axiom (forall b0: byte, b1: byte, b2: byte, b3: byte, c0: byte, c1: byte, c2: byte, c3: byte :: { v4.FourBytesToInt(b0, b1, b2, b3), v4.FourBytesToInt(c0, c1, c2, c3) } v4.FourBytesToInt(b0, b1, b2, b3) == v4.FourBytesToInt(c0, c1, c2, c3) ==> b0 == c0 && b1 == c1 && b2 == c2 && b3 == c3);
+
+axiom (forall x: int :: { v4.Base(x) } v4.INT_LEQ(v4.Base(x), x));
+
+axiom (forall a: int, t: name :: { v4.Match(a, v4.T.Ptr(t)) } v4.Match(a, v4.T.Ptr(t)) <==> v4.Field(a) == v4.T.Ptr(t));
+
+axiom (forall b: int, a: int, t: name :: { v4.MatchBase(b, a, v4.T.Ptr(t)) } v4.MatchBase(b, a, v4.T.Ptr(t)) <==> v4.Base(a) == b);
+
+axiom (forall v: int, t: name :: { v4.HasType(v, v4.T.Ptr(t)) } v4.HasType(v, v4.T.Ptr(t)) <==> v == 0 || (v4.INT_GT(v, 0) && v4.Match(v, t) && v4.MatchBase(v4.Base(v), v, t)));
+
+axiom (forall x: int, S: [int]bool :: { v4._S_op1__EXPR(S)[x] } v4._S_op1__EXPR(S)[x] <==> S[v4.op1__EXPRInv(x)]);
+
+axiom (forall x: int, S: [int]bool :: { v4._S_op1__EXPRInv(S)[x] } v4._S_op1__EXPRInv(S)[x] <==> S[v4.op1__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op1__EXPR(S) } S[x] ==> v4._S_op1__EXPR(S)[v4.op1__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op1__EXPRInv(S) } S[x] ==> v4._S_op1__EXPRInv(S)[v4.op1__EXPRInv(x)]);
+
+axiom (forall x: int :: { v4.op1__EXPR(x) } v4.op1__EXPR(x) == v4.INT_ADD(x, 4));
+
+axiom (forall x: int :: { v4.op1__EXPRInv(x) } v4.op1__EXPRInv(x) == v4.INT_SUB(x, 4));
+
+axiom (forall x: int :: { v4.op1__EXPR(x) } v4.op1__EXPR(x) == v4.PLUS(x, 1, 4));
+
+axiom (forall x: int, S: [int]bool :: { v4._S_op2__EXPR(S)[x] } v4._S_op2__EXPR(S)[x] <==> S[v4.op2__EXPRInv(x)]);
+
+axiom (forall x: int, S: [int]bool :: { v4._S_op2__EXPRInv(S)[x] } v4._S_op2__EXPRInv(S)[x] <==> S[v4.op2__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op2__EXPR(S) } S[x] ==> v4._S_op2__EXPR(S)[v4.op2__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op2__EXPRInv(S) } S[x] ==> v4._S_op2__EXPRInv(S)[v4.op2__EXPRInv(x)]);
+
+axiom (forall x: int :: { v4.op2__EXPR(x) } v4.op2__EXPR(x) == v4.INT_ADD(x, 8));
+
+axiom (forall x: int :: { v4.op2__EXPRInv(x) } v4.op2__EXPRInv(x) == v4.INT_SUB(x, 8));
+
+axiom (forall x: int :: { v4.op2__EXPR(x) } v4.op2__EXPR(x) == v4.PLUS(x, 1, 8));
+
+axiom (forall x: int, S: [int]bool :: { v4._S_oper__EXPR(S)[x] } v4._S_oper__EXPR(S)[x] <==> S[v4.oper__EXPRInv(x)]);
+
+axiom (forall x: int, S: [int]bool :: { v4._S_oper__EXPRInv(S)[x] } v4._S_oper__EXPRInv(S)[x] <==> S[v4.oper__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_oper__EXPR(S) } S[x] ==> v4._S_oper__EXPR(S)[v4.oper__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_oper__EXPRInv(S) } S[x] ==> v4._S_oper__EXPRInv(S)[v4.oper__EXPRInv(x)]);
+
+axiom (forall x: int :: { v4.oper__EXPR(x) } v4.oper__EXPR(x) == v4.INT_ADD(x, 0));
+
+axiom (forall x: int :: { v4.oper__EXPRInv(x) } v4.oper__EXPRInv(x) == v4.INT_SUB(x, 0));
+
+axiom (forall x: int :: { v4.oper__EXPR(x) } v4.oper__EXPR(x) == v4.PLUS(x, 1, 0));
+
+axiom (forall x: int, S: [int]bool :: { v4._S_result__EXPR(S)[x] } v4._S_result__EXPR(S)[x] <==> S[v4.result__EXPRInv(x)]);
+
+axiom (forall x: int, S: [int]bool :: { v4._S_result__EXPRInv(S)[x] } v4._S_result__EXPRInv(S)[x] <==> S[v4.result__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_result__EXPR(S) } S[x] ==> v4._S_result__EXPR(S)[v4.result__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_result__EXPRInv(S) } S[x] ==> v4._S_result__EXPRInv(S)[v4.result__EXPRInv(x)]);
+
+axiom (forall x: int :: { v4.result__EXPR(x) } v4.result__EXPR(x) == v4.INT_ADD(x, 12));
+
+axiom (forall x: int :: { v4.result__EXPRInv(x) } v4.result__EXPRInv(x) == v4.INT_SUB(x, 12));
+
+axiom (forall x: int :: { v4.result__EXPR(x) } v4.result__EXPR(x) == v4.PLUS(x, 1, 12));
+
+axiom (forall x: int, y: int :: { v4.INT_EQ(x, y): bool } v4.INT_EQ(x, y): bool <==> x == y);
+
+axiom (forall x: int, y: int :: { v4.INT_NEQ(x, y): bool } v4.INT_NEQ(x, y): bool <==> x != y);
+
+axiom (forall x: int, y: int :: { v4.INT_ADD(x, y): int } v4.INT_ADD(x, y): int == x + y);
+
+axiom (forall x: int, y: int :: { v4.INT_SUB(x, y): int } v4.INT_SUB(x, y): int == x - y);
+
+axiom (forall x: int, y: int :: { v4.INT_MULT(x, y): int } v4.INT_MULT(x, y): int == x * y);
+
+axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x / y);
+
+axiom (forall x: int, y: int :: { v4.INT_LT(x, y): bool } v4.INT_LT(x, y): bool <==> x < y);
+
+axiom (forall x: int, y: int :: { v4.INT_ULT(x, y): bool } v4.INT_ULT(x, y): bool <==> x < y);
+
+axiom (forall x: int, y: int :: { v4.INT_LEQ(x, y): bool } v4.INT_LEQ(x, y): bool <==> x <= y);
+
+axiom (forall x: int, y: int :: { v4.INT_ULEQ(x, y): bool } v4.INT_ULEQ(x, y): bool <==> x <= y);
+
+axiom (forall x: int, y: int :: { v4.INT_GT(x, y): bool } v4.INT_GT(x, y): bool <==> x > y);
+
+axiom (forall x: int, y: int :: { v4.INT_UGT(x, y): bool } v4.INT_UGT(x, y): bool <==> x > y);
+
+axiom (forall x: int, y: int :: { v4.INT_GEQ(x, y): bool } v4.INT_GEQ(x, y): bool <==> x >= y);
+
+axiom (forall x: int, y: int :: { v4.INT_UGEQ(x, y): bool } v4.INT_UGEQ(x, y): bool <==> x >= y);
+
+axiom (forall x: bv32, y: bv32 :: { v4.BV32_EQ(x, y): bool } v4.BV32_EQ(x, y): bool <==> x == y);
+
+axiom (forall x: bv32, y: bv32 :: { v4.BV32_NEQ(x, y): bool } v4.BV32_NEQ(x, y): bool <==> x != y);
+
+axiom (forall a: int, b: int, size: int :: { v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size) } v4.INT_LEQ(v4.INT_MULT(size, v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size)), v4.INT_SUB(a, b)) && v4.INT_LT(v4.INT_SUB(a, b), v4.INT_MULT(size, v4.INT_ADD(v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size), 1))));
+
+axiom (forall a: int, b: int, size: int :: { v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size) } v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, 1) == v4.INT_SUB(a, b));
+
+axiom (forall a: int, a_size: int, b: int :: { v4.MINUS_LEFT_PTR(a, a_size, b) } v4.MINUS_LEFT_PTR(a, a_size, b) == v4.INT_SUB(a, v4.INT_MULT(a_size, b)));
+
+axiom (forall a: int, a_size: int, b: int :: { v4.PLUS(a, a_size, b) } v4.PLUS(a, a_size, b) == v4.INT_ADD(a, v4.INT_MULT(a_size, b)));
+
+axiom (forall a: int, b: int :: { v4.MULT(a, b) } v4.MULT(a, b) == v4.INT_MULT(a, b));
+
+axiom (forall a: int, b: int :: { v4.DIV(a, b) } a >= 0 && b > 0 ==> b * v4.DIV(a, b) <= a && a < b * (v4.DIV(a, b) + 1));
+
+axiom (forall a: int, b: int :: { v4.DIV(a, b) } a >= 0 && b < 0 ==> b * v4.DIV(a, b) <= a && a < b * (v4.DIV(a, b) - 1));
+
+axiom (forall a: int, b: int :: { v4.DIV(a, b) } a < 0 && b > 0 ==> b * v4.DIV(a, b) >= a && a > b * (v4.DIV(a, b) - 1));
+
+axiom (forall a: int, b: int :: { v4.DIV(a, b) } a < 0 && b < 0 ==> b * v4.DIV(a, b) >= a && a > b * (v4.DIV(a, b) + 1));
+
+axiom v4.POW2(1);
+
+axiom v4.POW2(2);
+
+axiom v4.POW2(4);
+
+axiom v4.POW2(8);
+
+axiom v4.POW2(16);
+
+axiom v4.POW2(32);
+
+axiom v4.POW2(64);
+
+axiom v4.POW2(128);
+
+axiom v4.POW2(256);
+
+axiom v4.POW2(512);
+
+axiom v4.POW2(1024);
+
+axiom v4.POW2(2048);
+
+axiom v4.POW2(4096);
+
+axiom v4.POW2(8192);
+
+axiom v4.POW2(16384);
+
+axiom v4.POW2(32768);
+
+axiom v4.POW2(65536);
+
+axiom v4.POW2(131072);
+
+axiom v4.POW2(262144);
+
+axiom v4.POW2(524288);
+
+axiom v4.POW2(1048576);
+
+axiom v4.POW2(2097152);
+
+axiom v4.POW2(4194304);
+
+axiom v4.POW2(8388608);
+
+axiom v4.POW2(16777216);
+
+axiom v4.POW2(33554432);
+
+axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } a == b ==> v4.BIT_BAND(a, b) == a);
+
+axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } v4.POW2(a) && v4.POW2(b) && a != b ==> v4.BIT_BAND(a, b) == 0);
+
+axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } a == 0 || b == 0 ==> v4.BIT_BAND(a, b) == 0);
+
+axiom (forall a: bool, b: int, c: int :: { v4.choose(a, b, c) } a ==> v4.choose(a, b, c) == b);
+
+axiom (forall a: bool, b: int, c: int :: { v4.choose(a, b, c) } !a ==> v4.choose(a, b, c) == c);
+
+axiom (forall a: bool :: { v4.LIFT(a) } a <==> v4.LIFT(a) != 0);
+
+axiom (forall a: int :: { v4.PTR_NOT(a) } a == 0 ==> v4.PTR_NOT(a) != 0);
+
+axiom (forall a: int :: { v4.PTR_NOT(a) } a != 0 ==> v4.PTR_NOT(a) == 0);
+
+axiom (forall a: int :: { v4.NULL_CHECK(a) } a == 0 ==> v4.NULL_CHECK(a) != 0);
+
+axiom (forall a: int :: { v4.NULL_CHECK(a) } a != 0 ==> v4.NULL_CHECK(a) == 0);
+
+axiom (forall n: int, x: int, y: int :: { v4.AtLeast(n, x)[y] } v4.AtLeast(n, x)[y] ==> v4.INT_LEQ(x, y) && v4.Rep(n, x) == v4.Rep(n, y));
+
+axiom (forall n: int, x: int, y: int :: { v4.AtLeast(n, x), v4.Rep(n, x), v4.Rep(n, y) } v4.INT_LEQ(x, y) && v4.Rep(n, x) == v4.Rep(n, y) ==> v4.AtLeast(n, x)[y]);
+
+axiom (forall n: int, x: int :: { v4.AtLeast(n, x) } v4.AtLeast(n, x)[x]);
+
+axiom (forall n: int, x: int, z: int :: { v4.PLUS(x, n, z) } v4.Rep(n, x) == v4.Rep(n, v4.PLUS(x, n, z)));
+
+axiom (forall n: int, x: int :: { v4.Rep(n, x) } (exists k: int :: v4.INT_SUB(v4.Rep(n, x), x) == v4.INT_MULT(n, k)));
+
+axiom (forall x: int, n: int, z: int :: { v4.Array(x, n, z) } v4.INT_LEQ(z, 0) ==> v4.Equal(v4.Array(x, n, z), v4.Empty()));
+
+axiom (forall x: int, n: int, z: int :: { v4.Array(x, n, z) } v4.INT_GT(z, 0) ==> v4.Equal(v4.Array(x, n, z), v4.Difference(v4.AtLeast(n, x), v4.AtLeast(n, v4.PLUS(x, n, z)))));
+
+axiom (forall x: int :: !v4.Empty()[x]);
+
+axiom (forall x: int :: v4.SetTrue()[x]);
+
+axiom (forall x: int, y: int :: { v4.Singleton(y)[x] } v4.Singleton(y)[x] <==> x == y);
+
+axiom (forall y: int :: { v4.Singleton(y) } v4.Singleton(y)[y]);
+
+axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Union(S, T)[x] } { v4.Union(S, T), S[x] } { v4.Union(S, T), T[x] } v4.Union(S, T)[x] <==> S[x] || T[x]);
+
+axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Intersection(S, T)[x] } { v4.Intersection(S, T), S[x] } { v4.Intersection(S, T), T[x] } v4.Intersection(S, T)[x] <==> S[x] && T[x]);
+
+axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Difference(S, T)[x] } { v4.Difference(S, T), S[x] } { v4.Difference(S, T), T[x] } v4.Difference(S, T)[x] <==> S[x] && !T[x]);
+
+axiom (forall S: [int]bool, T: [int]bool :: { v4.Equal(S, T) } v4.Equal(S, T) <==> v4.Subset(S, T) && v4.Subset(T, S));
+
+axiom (forall x: int, S: [int]bool, T: [int]bool :: { S[x], v4.Subset(S, T) } { T[x], v4.Subset(S, T) } S[x] && v4.Subset(S, T) ==> T[x]);
+
+axiom (forall S: [int]bool, T: [int]bool :: { v4.Subset(S, T) } v4.Subset(S, T) || (exists x: int :: S[x] && !T[x]));
+
+axiom (forall x: int, S: [int]bool, T: [int]bool :: { S[x], v4.Disjoint(S, T) } { T[x], v4.Disjoint(S, T) } !(S[x] && v4.Disjoint(S, T) && T[x]));
+
+axiom (forall S: [int]bool, T: [int]bool :: { v4.Disjoint(S, T) } v4.Disjoint(S, T) || (exists x: int :: S[x] && T[x]));
+
+axiom (forall f: [int]int, x: int :: { v4.Inverse(f, f[x]) } v4.Inverse(f, f[x])[x]);
+
+axiom (forall f: [int]int, x: int, y: int :: { v4.Inverse(f, y), f[x] } v4.Inverse(f, y)[x] ==> f[x] == y);
+
+axiom (forall f: [int]int, x: int, y: int :: { v4.Inverse(f[x := y], y) } v4.Equal(v4.Inverse(f[x := y], y), v4.Union(v4.Inverse(f, y), v4.Singleton(x))));
+
+axiom (forall f: [int]int, x: int, y: int, z: int :: { v4.Inverse(f[x := y], z) } y == z || v4.Equal(v4.Inverse(f[x := y], z), v4.Difference(v4.Inverse(f, z), v4.Singleton(x))));
+
+axiom (forall x: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M)[x] } v4.Dereference(S, M)[x] ==> (exists y: int :: x == M[y] && S[y]));
+
+axiom (forall x: int, S: [int]bool, M: [int]int :: { M[x], S[x], v4.Dereference(S, M) } S[x] ==> v4.Dereference(S, M)[M[x]]);
+
+axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } !S[x] ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Dereference(S, M)));
+
+axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } S[x] && v4.Equal(v4.Intersection(v4.Inverse(M, M[x]), S), v4.Singleton(x)) ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Union(v4.Difference(v4.Dereference(S, M), v4.Singleton(M[x])), v4.Singleton(y))));
+
+axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } S[x] && !v4.Equal(v4.Intersection(v4.Inverse(M, M[x]), S), v4.Singleton(x)) ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Union(v4.Dereference(S, M), v4.Singleton(y))));
+
+axiom (forall M: [name][int]int, x: int :: { v4.Unified(M)[x] } v4.Unified(M)[x] == M[v4.Field(x)][x]);
+
+axiom (forall M: [name][int]int, x: int, y: int :: { v4.Unified(M[v4.Field(x) := M[v4.Field(x)][x := y]]) } v4.Unified(M[v4.Field(x) := M[v4.Field(x)][x := y]]) == v4.Unified(M)[x := y]);
+
+procedure v4.havoc_assert(i: int);
+
+
+
+procedure v4.havoc_assume(i: int);
+
+
+
+procedure v4.__HAVOC_free(a: int);
+
+
+
+procedure v4.__HAVOC_malloc(obj_size: int) returns (new: int);
+ free ensures new == _uf_v4.__HAVOC_malloc_new(obj_size);
+
+
+
+procedure v4.__HAVOC_det_malloc(obj_size: int) returns (new: int);
+ free ensures new == _uf_v4.__HAVOC_det_malloc_new(obj_size);
+
+
+
+procedure v4.__HAVOC_memset_split_1(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int);
+ free ensures ret == _uf_v4.__HAVOC_memset_split_1_ret(A, p, c, n);
+
+
+
+procedure v4.__HAVOC_memset_split_2(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int);
+ free ensures ret == _uf_v4.__HAVOC_memset_split_2_ret(A, p, c, n);
+
+
+
+procedure v4.__HAVOC_memset_split_4(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int);
+ free ensures ret == _uf_v4.__HAVOC_memset_split_4_ret(A, p, c, n);
+
+
+
+procedure v4.nondet_choice() returns (x: int);
+ free ensures x == _uf_v4.nondet_choice_x();
+
+
+
+procedure v4.det_choice() returns (x: int);
+ free ensures x == _uf_v4.det_choice_x();
+
+
+
+procedure v4._strdup(str: int) returns (new: int);
+ free ensures new == _uf_v4._strdup_new(str);
+
+
+
+procedure v4._xstrcasecmp(a0: int, a1: int) returns (ret: int);
+ free ensures ret == _uf_v4._xstrcasecmp_ret(a0, a1);
+
+
+
+procedure v4._xstrcmp(a0: int, a1: int) returns (ret: int);
+ free ensures ret == _uf_v4._xstrcmp_ret(a0, a1);
+
+
+
+procedure v4.UnsignedAdd(a0: int, a1: int) returns (ret: int);
+
+
+
+procedure v4.UnsignedSub(a0: int, a1: int) returns (ret: int);
+
+
+
+procedure {:inline 1} v4.Eval(e_.1: int);
+ modifies v4.Mem_T.result__EXPR;
+ free ensures v4.Mem_T.result__EXPR == _uf_v4.Eval_v4.Mem_T.result__EXPR(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned));
+
+
+
+procedure v4.EvalEntry1(e_.1: int, outval_.1: int);
+ modifies v4.isUnsigned, v4.Mem_T.result__EXPR, v4.Mem_T.INT4;
+ free ensures v4.isUnsigned == _uf_v4.EvalEntry1_v4.isUnsigned(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned));
+ free ensures v4.Mem_T.result__EXPR == _uf_v4.EvalEntry1_v4.Mem_T.result__EXPR(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned));
+ free ensures v4.Mem_T.INT4 == _uf_v4.EvalEntry1_v4.Mem_T.INT4(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned));
+
+
+
+procedure v4.EvalEntry2(e_.1: int);
+ modifies v4.isUnsigned, v4.Mem_T.result__EXPR;
+ free ensures v4.isUnsigned == _uf_v4.EvalEntry2_v4.isUnsigned(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned));
+ free ensures v4.Mem_T.result__EXPR == _uf_v4.EvalEntry2_v4.Mem_T.result__EXPR(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned));
+
+
+
+procedure v4.__havoc_heapglobal_init();
+
+
+
+implementation {:inline 1} v4.Eval(e_.1: int)
+{
+ var havoc_stringTemp: int;
+ var condVal: int;
+ var a1: int;
+ var a2: int;
+ var e: int;
+ var op: int;
+ var res: int;
+ var result.UnsignedAdd$1: int;
+ var result.UnsignedSub$2: int;
+ var tempBoogie0: int;
+ var tempBoogie1: int;
+ var tempBoogie2: int;
+ var tempBoogie3: int;
+ var tempBoogie4: int;
+ var tempBoogie5: int;
+ var tempBoogie6: int;
+ var tempBoogie7: int;
+ var tempBoogie8: int;
+ var tempBoogie9: int;
+ var tempBoogie10: int;
+ var tempBoogie11: int;
+ var tempBoogie12: int;
+ var tempBoogie13: int;
+ var tempBoogie14: int;
+ var tempBoogie15: int;
+ var tempBoogie16: int;
+ var tempBoogie17: int;
+ var tempBoogie18: int;
+ var tempBoogie19: int;
+ var __havoc_dummy_return: int;
+
+ anon0#2:
+ havoc_stringTemp := 0;
+ goto start#2;
+
+ start#2:
+ assume v4.INT_LT(e_.1, v4.alloc);
+ a1 := 0;
+ a2 := 0;
+ e := 0;
+ op := 0;
+ res := 0;
+ result.UnsignedAdd$1 := 0;
+ result.UnsignedSub$2 := 0;
+ e := e_.1;
+ goto label_3#2;
+
+ label_3#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true;
+ goto label_4#2;
+
+ label_4#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true;
+ goto label_5#2;
+
+ label_5#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true;
+ goto label_6#2;
+
+ label_6#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true;
+ goto label_7#2;
+
+ label_7#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 21} true;
+ assert true;
+ op := v4.Mem_T.oper__EXPR[v4.oper__EXPR(e)];
+ assume v4.value_is(v4.__ctobpl_const_1, op);
+ assume v4.value_is(v4.__ctobpl_const_2, e);
+ assume v4.value_is(v4.__ctobpl_const_3, v4.Mem_T.oper__EXPR[v4.oper__EXPR(e)]);
+ goto label_8#2;
+
+ label_8#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 22} true;
+ assert true;
+ a1 := v4.Mem_T.op1__EXPR[v4.op1__EXPR(e)];
+ assume v4.value_is(v4.__ctobpl_const_4, a1);
+ assume v4.value_is(v4.__ctobpl_const_5, e);
+ assume v4.value_is(v4.__ctobpl_const_6, v4.Mem_T.op1__EXPR[v4.op1__EXPR(e)]);
+ goto label_9#2;
+
+ label_9#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 23} true;
+ assert true;
+ a2 := v4.Mem_T.op2__EXPR[v4.op2__EXPR(e)];
+ assume v4.value_is(v4.__ctobpl_const_7, a2);
+ assume v4.value_is(v4.__ctobpl_const_8, e);
+ assume v4.value_is(v4.__ctobpl_const_9, v4.Mem_T.op2__EXPR[v4.op2__EXPR(e)]);
+ goto label_10#2;
+
+ label_10#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 24} true;
+ res := 0 - 1;
+ assume v4.value_is(v4.__ctobpl_const_10, res);
+ goto label_11#2;
+
+ label_11#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 26} true;
+ goto label_11_case_0#2, label_11_case_1#2, label_11_case_2#2;
+
+ label_11_case_2#2:
+ assume v4.INT_EQ(op, 2);
+ assume v4.value_is(v4.__ctobpl_const_11, op);
+ goto label_14#2;
+
+ label_14#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 35} true;
+ goto label_14_true#2, label_14_false#2;
+
+ label_14_false#2:
+ assume v4.isUnsigned == 0;
+ assume v4.value_is(v4.__ctobpl_const_16, v4.isUnsigned);
+ goto label_15#2;
+
+ label_15#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 38} true;
+ res := v4.MINUS_BOTH_PTR_OR_BOTH_INT(a1, a2, 1);
+ assume v4.value_is(v4.__ctobpl_const_17, res);
+ assume v4.value_is(v4.__ctobpl_const_18, a1);
+ assume v4.value_is(v4.__ctobpl_const_19, a2);
+ goto label_12#2;
+
+ label_14_true#2:
+ assume v4.isUnsigned != 0;
+ assume v4.value_is(v4.__ctobpl_const_16, v4.isUnsigned);
+ goto label_16#2;
+
+ label_16#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 36} true;
+ call result.UnsignedSub$2 := v4.UnsignedSub(a1, a2);
+ assume v4.value_is(v4.__ctobpl_const_20, a1);
+ assume v4.value_is(v4.__ctobpl_const_21, a2);
+ assume v4.value_is(v4.__ctobpl_const_22, a1);
+ assume v4.value_is(v4.__ctobpl_const_23, a2);
+ goto label_19#2;
+
+ label_19#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 36} true;
+ res := result.UnsignedSub$2;
+ assume v4.value_is(v4.__ctobpl_const_24, res);
+ assume v4.value_is(v4.__ctobpl_const_25, result.UnsignedSub$2);
+ goto label_12#2;
+
+ label_11_case_1#2:
+ assume v4.INT_EQ(op, 1);
+ assume v4.value_is(v4.__ctobpl_const_11, op);
+ goto label_13#2;
+
+ label_13#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 29} true;
+ goto label_13_true#2, label_13_false#2;
+
+ label_13_false#2:
+ assume v4.isUnsigned == 0;
+ assume v4.value_is(v4.__ctobpl_const_15, v4.isUnsigned);
+ goto label_20#2;
+
+ label_20#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 32} true;
+ res := v4.PLUS(a1, 1, a2);
+ assume v4.value_is(v4.__ctobpl_const_26, res);
+ assume v4.value_is(v4.__ctobpl_const_27, a1);
+ assume v4.value_is(v4.__ctobpl_const_28, a2);
+ goto label_12#2;
+
+ label_13_true#2:
+ assume v4.isUnsigned != 0;
+ assume v4.value_is(v4.__ctobpl_const_15, v4.isUnsigned);
+ goto label_21#2;
+
+ label_21#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 30} true;
+ call result.UnsignedAdd$1 := v4.UnsignedAdd(a1, a2);
+ assume v4.value_is(v4.__ctobpl_const_29, a1);
+ assume v4.value_is(v4.__ctobpl_const_30, a2);
+ assume v4.value_is(v4.__ctobpl_const_31, a1);
+ assume v4.value_is(v4.__ctobpl_const_32, a2);
+ goto label_24#2;
+
+ label_24#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 30} true;
+ res := result.UnsignedAdd$1;
+ assume v4.value_is(v4.__ctobpl_const_33, res);
+ assume v4.value_is(v4.__ctobpl_const_34, result.UnsignedAdd$1);
+ goto label_12#2;
+
+ label_11_case_0#2:
+ assume v4.INT_NEQ(op, 1);
+ assume v4.INT_NEQ(op, 2);
+ assume v4.value_is(v4.__ctobpl_const_11, op);
+ goto label_12#2;
+
+ label_12#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 41} true;
+ assert true;
+ v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR[v4.result__EXPR(e) := res];
+ assume v4.value_is(v4.__ctobpl_const_12, e);
+ assume v4.value_is(v4.__ctobpl_const_13, v4.Mem_T.result__EXPR[v4.result__EXPR(e)]);
+ assume v4.value_is(v4.__ctobpl_const_14, res);
+ goto label_1#2;
+
+ label_1#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 42} true;
+ return;
+}
+
+
+
+implementation v4.EvalEntry1(e_.1: int, outval_.1: int)
+{
+ var havoc_stringTemp: int;
+ var condVal: int;
+ var e: int;
+ var outval: int;
+ var tempBoogie0: int;
+ var tempBoogie1: int;
+ var tempBoogie2: int;
+ var tempBoogie3: int;
+ var tempBoogie4: int;
+ var tempBoogie5: int;
+ var tempBoogie6: int;
+ var tempBoogie7: int;
+ var tempBoogie8: int;
+ var tempBoogie9: int;
+ var tempBoogie10: int;
+ var tempBoogie11: int;
+ var tempBoogie12: int;
+ var tempBoogie13: int;
+ var tempBoogie14: int;
+ var tempBoogie15: int;
+ var tempBoogie16: int;
+ var tempBoogie17: int;
+ var tempBoogie18: int;
+ var tempBoogie19: int;
+ var __havoc_dummy_return: int;
+
+ anon0#2:
+ havoc_stringTemp := 0;
+ goto start#2;
+
+ start#2:
+ assume v4.INT_LT(e_.1, v4.alloc);
+ assume v4.INT_LT(outval_.1, v4.alloc);
+ e := 0;
+ outval := 0;
+ e := e_.1;
+ outval := outval_.1;
+ goto label_3#2;
+
+ label_3#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 47} true;
+ v4.isUnsigned := 1;
+ assume v4.value_is(v4.__ctobpl_const_35, v4.isUnsigned);
+ goto label_4#2;
+
+ label_4#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 48} true;
+ call v4.Eval(e);
+ assume v4.value_is(v4.__ctobpl_const_36, e);
+ assume v4.value_is(v4.__ctobpl_const_37, e);
+ goto label_7#2;
+
+ label_7#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 49} true;
+ assert true;
+ assert true;
+ v4.Mem_T.INT4 := v4.Mem_T.INT4[outval := v4.Mem_T.result__EXPR[v4.result__EXPR(e)]];
+ assume v4.value_is(v4.__ctobpl_const_38, outval);
+ assume v4.value_is(v4.__ctobpl_const_39, v4.Mem_T.INT4[outval]);
+ assume v4.value_is(v4.__ctobpl_const_40, e);
+ assume v4.value_is(v4.__ctobpl_const_41, v4.Mem_T.result__EXPR[v4.result__EXPR(e)]);
+ goto label_1#2;
+
+ label_1#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 50} true;
+ return;
+}
+
+
+
+implementation v4.EvalEntry2(e_.1: int)
+{
+ var havoc_stringTemp: int;
+ var condVal: int;
+ var e: int;
+ var tempBoogie0: int;
+ var tempBoogie1: int;
+ var tempBoogie2: int;
+ var tempBoogie3: int;
+ var tempBoogie4: int;
+ var tempBoogie5: int;
+ var tempBoogie6: int;
+ var tempBoogie7: int;
+ var tempBoogie8: int;
+ var tempBoogie9: int;
+ var tempBoogie10: int;
+ var tempBoogie11: int;
+ var tempBoogie12: int;
+ var tempBoogie13: int;
+ var tempBoogie14: int;
+ var tempBoogie15: int;
+ var tempBoogie16: int;
+ var tempBoogie17: int;
+ var tempBoogie18: int;
+ var tempBoogie19: int;
+ var __havoc_dummy_return: int;
+
+ anon0#2:
+ havoc_stringTemp := 0;
+ goto start#2;
+
+ start#2:
+ assume v4.INT_LT(e_.1, v4.alloc);
+ e := 0;
+ e := e_.1;
+ goto label_3#2;
+
+ label_3#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 54} true;
+ v4.isUnsigned := 0;
+ assume v4.value_is(v4.__ctobpl_const_42, v4.isUnsigned);
+ goto label_4#2;
+
+ label_4#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 55} true;
+ call v4.Eval(e);
+ assume v4.value_is(v4.__ctobpl_const_43, e);
+ assume v4.value_is(v4.__ctobpl_const_44, e);
+ goto label_1#2;
+
+ label_1#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 56} true;
+ return;
+}
+
+
+
+implementation v4.__havoc_heapglobal_init()
+{
+
+ anon0#2:
+ return;
+}
+
+
+
+var v2.Mem: [name][int]int;
+
+var v2.alloc: int;
+
+var v2.Mem_T.INT4: [int]int;
+
+var v2.Mem_T.op1__EXPR: [int]int;
+
+var v2.Mem_T.op2__EXPR: [int]int;
+
+var v2.Mem_T.oper__EXPR: [int]int;
+
+var v2.Mem_T.result__EXPR: [int]int;
+
+var v2.detChoiceCnt: int;
+
+var v2.Res_KERNEL_SOURCE: [int]int;
+
+var v2.Res_PROBED: [int]int;
+
+const unique v2.T.oper__EXPR: name;
+
+const unique v2.T.op1__EXPR: name;
+
+const unique v2.T.op2__EXPR: name;
+
+const unique v2.T.result__EXPR: name;
+
+const unique v2.T.INT4: name;
+
+const unique v2.T.PINT4: name;
+
+const unique v2.T.PPINT4: name;
+
+const unique v2.T.PP_EXPR: name;
+
+const unique v2.T.P_EXPR: name;
+
+const unique v2.T._EXPR: name;
+
+const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 21} unique v2.__ctobpl_const_7: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 21} unique v2.__ctobpl_const_8: int;
+
+const {:model_const "e->oper"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 19} unique v2.__ctobpl_const_3: int;
+
+const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 20} unique v2.__ctobpl_const_4: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 20} unique v2.__ctobpl_const_5: int;
+
+const {:model_const "e->op1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 20} unique v2.__ctobpl_const_6: int;
+
+const {:model_const "e->op2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 21} unique v2.__ctobpl_const_9: int;
+
+const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 22} unique v2.__ctobpl_const_10: int;
+
+const {:model_const "op"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 24} unique v2.__ctobpl_const_11: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 35} unique v2.__ctobpl_const_12: int;
+
+const {:model_const "e->result"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 35} unique v2.__ctobpl_const_13: int;
+
+const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 35} unique v2.__ctobpl_const_14: int;
+
+const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 27} unique v2.__ctobpl_const_15: int;
+
+const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 27} unique v2.__ctobpl_const_16: int;
+
+const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 27} unique v2.__ctobpl_const_17: int;
+
+const {:model_const "res"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 29} unique v2.__ctobpl_const_18: int;
+
+const {:model_const "a1"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 29} unique v2.__ctobpl_const_19: int;
+
+const {:model_const "a2"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 29} unique v2.__ctobpl_const_20: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 40} unique v2.__ctobpl_const_21: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 40} unique v2.__ctobpl_const_22: int;
+
+const {:model_const "outval"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 41} unique v2.__ctobpl_const_23: int;
+
+const {:model_const "*outval"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 41} unique v2.__ctobpl_const_24: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 41} unique v2.__ctobpl_const_25: int;
+
+const {:model_const "e->result"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 41} unique v2.__ctobpl_const_26: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 46} unique v2.__ctobpl_const_27: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 46} unique v2.__ctobpl_const_28: int;
+
+const {:model_const "op"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 19} unique v2.__ctobpl_const_1: int;
+
+const {:model_const "e"} {:sourceFile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceLine 19} unique v2.__ctobpl_const_2: int;
+
+axiom (forall b0: byte, c0: byte :: { v4.OneByteToInt(b0), v4.OneByteToInt(c0) } v4.OneByteToInt(b0) == v4.OneByteToInt(c0) ==> b0 == c0);
+
+axiom (forall b0: byte, b1: byte, c0: byte, c1: byte :: { v4.TwoBytesToInt(b0, b1), v4.TwoBytesToInt(c0, c1) } v4.TwoBytesToInt(b0, b1) == v4.TwoBytesToInt(c0, c1) ==> b0 == c0 && b1 == c1);
+
+axiom (forall b0: byte, b1: byte, b2: byte, b3: byte, c0: byte, c1: byte, c2: byte, c3: byte :: { v4.FourBytesToInt(b0, b1, b2, b3), v4.FourBytesToInt(c0, c1, c2, c3) } v4.FourBytesToInt(b0, b1, b2, b3) == v4.FourBytesToInt(c0, c1, c2, c3) ==> b0 == c0 && b1 == c1 && b2 == c2 && b3 == c3);
+
+axiom (forall x: int :: { v4.Base(x) } v4.INT_LEQ(v4.Base(x), x));
+
+axiom (forall a: int, t: name :: { v4.Match(a, v4.T.Ptr(t)) } v4.Match(a, v4.T.Ptr(t)) <==> v4.Field(a) == v4.T.Ptr(t));
+
+axiom (forall b: int, a: int, t: name :: { v4.MatchBase(b, a, v4.T.Ptr(t)) } v4.MatchBase(b, a, v4.T.Ptr(t)) <==> v4.Base(a) == b);
+
+axiom (forall v: int, t: name :: { v4.HasType(v, v4.T.Ptr(t)) } v4.HasType(v, v4.T.Ptr(t)) <==> v == 0 || (v4.INT_GT(v, 0) && v4.Match(v, t) && v4.MatchBase(v4.Base(v), v, t)));
+
+axiom (forall x: int, S: [int]bool :: { v4._S_op1__EXPR(S)[x] } v4._S_op1__EXPR(S)[x] <==> S[v4.op1__EXPRInv(x)]);
+
+axiom (forall x: int, S: [int]bool :: { v4._S_op1__EXPRInv(S)[x] } v4._S_op1__EXPRInv(S)[x] <==> S[v4.op1__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op1__EXPR(S) } S[x] ==> v4._S_op1__EXPR(S)[v4.op1__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op1__EXPRInv(S) } S[x] ==> v4._S_op1__EXPRInv(S)[v4.op1__EXPRInv(x)]);
+
+axiom (forall x: int :: { v4.op1__EXPR(x) } v4.op1__EXPR(x) == v4.INT_ADD(x, 4));
+
+axiom (forall x: int :: { v4.op1__EXPRInv(x) } v4.op1__EXPRInv(x) == v4.INT_SUB(x, 4));
+
+axiom (forall x: int :: { v4.op1__EXPR(x) } v4.op1__EXPR(x) == v4.PLUS(x, 1, 4));
+
+axiom (forall x: int, S: [int]bool :: { v4._S_op2__EXPR(S)[x] } v4._S_op2__EXPR(S)[x] <==> S[v4.op2__EXPRInv(x)]);
+
+axiom (forall x: int, S: [int]bool :: { v4._S_op2__EXPRInv(S)[x] } v4._S_op2__EXPRInv(S)[x] <==> S[v4.op2__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op2__EXPR(S) } S[x] ==> v4._S_op2__EXPR(S)[v4.op2__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_op2__EXPRInv(S) } S[x] ==> v4._S_op2__EXPRInv(S)[v4.op2__EXPRInv(x)]);
+
+axiom (forall x: int :: { v4.op2__EXPR(x) } v4.op2__EXPR(x) == v4.INT_ADD(x, 8));
+
+axiom (forall x: int :: { v4.op2__EXPRInv(x) } v4.op2__EXPRInv(x) == v4.INT_SUB(x, 8));
+
+axiom (forall x: int :: { v4.op2__EXPR(x) } v4.op2__EXPR(x) == v4.PLUS(x, 1, 8));
+
+axiom (forall x: int, S: [int]bool :: { v4._S_oper__EXPR(S)[x] } v4._S_oper__EXPR(S)[x] <==> S[v4.oper__EXPRInv(x)]);
+
+axiom (forall x: int, S: [int]bool :: { v4._S_oper__EXPRInv(S)[x] } v4._S_oper__EXPRInv(S)[x] <==> S[v4.oper__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_oper__EXPR(S) } S[x] ==> v4._S_oper__EXPR(S)[v4.oper__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_oper__EXPRInv(S) } S[x] ==> v4._S_oper__EXPRInv(S)[v4.oper__EXPRInv(x)]);
+
+axiom (forall x: int :: { v4.oper__EXPR(x) } v4.oper__EXPR(x) == v4.INT_ADD(x, 0));
+
+axiom (forall x: int :: { v4.oper__EXPRInv(x) } v4.oper__EXPRInv(x) == v4.INT_SUB(x, 0));
+
+axiom (forall x: int :: { v4.oper__EXPR(x) } v4.oper__EXPR(x) == v4.PLUS(x, 1, 0));
+
+axiom (forall x: int, S: [int]bool :: { v4._S_result__EXPR(S)[x] } v4._S_result__EXPR(S)[x] <==> S[v4.result__EXPRInv(x)]);
+
+axiom (forall x: int, S: [int]bool :: { v4._S_result__EXPRInv(S)[x] } v4._S_result__EXPRInv(S)[x] <==> S[v4.result__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_result__EXPR(S) } S[x] ==> v4._S_result__EXPR(S)[v4.result__EXPR(x)]);
+
+axiom (forall x: int, S: [int]bool :: { S[x], v4._S_result__EXPRInv(S) } S[x] ==> v4._S_result__EXPRInv(S)[v4.result__EXPRInv(x)]);
+
+axiom (forall x: int :: { v4.result__EXPR(x) } v4.result__EXPR(x) == v4.INT_ADD(x, 12));
+
+axiom (forall x: int :: { v4.result__EXPRInv(x) } v4.result__EXPRInv(x) == v4.INT_SUB(x, 12));
+
+axiom (forall x: int :: { v4.result__EXPR(x) } v4.result__EXPR(x) == v4.PLUS(x, 1, 12));
+
+axiom (forall x: int, y: int :: { v4.INT_EQ(x, y): bool } v4.INT_EQ(x, y): bool <==> x == y);
+
+axiom (forall x: int, y: int :: { v4.INT_NEQ(x, y): bool } v4.INT_NEQ(x, y): bool <==> x != y);
+
+axiom (forall x: int, y: int :: { v4.INT_ADD(x, y): int } v4.INT_ADD(x, y): int == x + y);
+
+axiom (forall x: int, y: int :: { v4.INT_SUB(x, y): int } v4.INT_SUB(x, y): int == x - y);
+
+axiom (forall x: int, y: int :: { v4.INT_MULT(x, y): int } v4.INT_MULT(x, y): int == x * y);
+
+axiom (forall x: int, y: int :: { v4.INT_DIV(x, y): int } v4.INT_DIV(x, y): int == x / y);
+
+axiom (forall x: int, y: int :: { v4.INT_LT(x, y): bool } v4.INT_LT(x, y): bool <==> x < y);
+
+axiom (forall x: int, y: int :: { v4.INT_ULT(x, y): bool } v4.INT_ULT(x, y): bool <==> x < y);
+
+axiom (forall x: int, y: int :: { v4.INT_LEQ(x, y): bool } v4.INT_LEQ(x, y): bool <==> x <= y);
+
+axiom (forall x: int, y: int :: { v4.INT_ULEQ(x, y): bool } v4.INT_ULEQ(x, y): bool <==> x <= y);
+
+axiom (forall x: int, y: int :: { v4.INT_GT(x, y): bool } v4.INT_GT(x, y): bool <==> x > y);
+
+axiom (forall x: int, y: int :: { v4.INT_UGT(x, y): bool } v4.INT_UGT(x, y): bool <==> x > y);
+
+axiom (forall x: int, y: int :: { v4.INT_GEQ(x, y): bool } v4.INT_GEQ(x, y): bool <==> x >= y);
+
+axiom (forall x: int, y: int :: { v4.INT_UGEQ(x, y): bool } v4.INT_UGEQ(x, y): bool <==> x >= y);
+
+axiom (forall x: bv32, y: bv32 :: { v4.BV32_EQ(x, y): bool } v4.BV32_EQ(x, y): bool <==> x == y);
+
+axiom (forall x: bv32, y: bv32 :: { v4.BV32_NEQ(x, y): bool } v4.BV32_NEQ(x, y): bool <==> x != y);
+
+axiom (forall a: int, b: int, size: int :: { v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size) } v4.INT_LEQ(v4.INT_MULT(size, v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size)), v4.INT_SUB(a, b)) && v4.INT_LT(v4.INT_SUB(a, b), v4.INT_MULT(size, v4.INT_ADD(v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size), 1))));
+
+axiom (forall a: int, b: int, size: int :: { v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, size) } v4.MINUS_BOTH_PTR_OR_BOTH_INT(a, b, 1) == v4.INT_SUB(a, b));
+
+axiom (forall a: int, a_size: int, b: int :: { v4.MINUS_LEFT_PTR(a, a_size, b) } v4.MINUS_LEFT_PTR(a, a_size, b) == v4.INT_SUB(a, v4.INT_MULT(a_size, b)));
+
+axiom (forall a: int, a_size: int, b: int :: { v4.PLUS(a, a_size, b) } v4.PLUS(a, a_size, b) == v4.INT_ADD(a, v4.INT_MULT(a_size, b)));
+
+axiom (forall a: int, b: int :: { v4.MULT(a, b) } v4.MULT(a, b) == v4.INT_MULT(a, b));
+
+axiom (forall a: int, b: int :: { v4.DIV(a, b) } a >= 0 && b > 0 ==> b * v4.DIV(a, b) <= a && a < b * (v4.DIV(a, b) + 1));
+
+axiom (forall a: int, b: int :: { v4.DIV(a, b) } a >= 0 && b < 0 ==> b * v4.DIV(a, b) <= a && a < b * (v4.DIV(a, b) - 1));
+
+axiom (forall a: int, b: int :: { v4.DIV(a, b) } a < 0 && b > 0 ==> b * v4.DIV(a, b) >= a && a > b * (v4.DIV(a, b) - 1));
+
+axiom (forall a: int, b: int :: { v4.DIV(a, b) } a < 0 && b < 0 ==> b * v4.DIV(a, b) >= a && a > b * (v4.DIV(a, b) + 1));
+
+axiom v4.POW2(1);
+
+axiom v4.POW2(2);
+
+axiom v4.POW2(4);
+
+axiom v4.POW2(8);
+
+axiom v4.POW2(16);
+
+axiom v4.POW2(32);
+
+axiom v4.POW2(64);
+
+axiom v4.POW2(128);
+
+axiom v4.POW2(256);
+
+axiom v4.POW2(512);
+
+axiom v4.POW2(1024);
+
+axiom v4.POW2(2048);
+
+axiom v4.POW2(4096);
+
+axiom v4.POW2(8192);
+
+axiom v4.POW2(16384);
+
+axiom v4.POW2(32768);
+
+axiom v4.POW2(65536);
+
+axiom v4.POW2(131072);
+
+axiom v4.POW2(262144);
+
+axiom v4.POW2(524288);
+
+axiom v4.POW2(1048576);
+
+axiom v4.POW2(2097152);
+
+axiom v4.POW2(4194304);
+
+axiom v4.POW2(8388608);
+
+axiom v4.POW2(16777216);
+
+axiom v4.POW2(33554432);
+
+axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } a == b ==> v4.BIT_BAND(a, b) == a);
+
+axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } v4.POW2(a) && v4.POW2(b) && a != b ==> v4.BIT_BAND(a, b) == 0);
+
+axiom (forall a: int, b: int :: { v4.BIT_BAND(a, b) } a == 0 || b == 0 ==> v4.BIT_BAND(a, b) == 0);
+
+axiom (forall a: bool, b: int, c: int :: { v4.choose(a, b, c) } a ==> v4.choose(a, b, c) == b);
+
+axiom (forall a: bool, b: int, c: int :: { v4.choose(a, b, c) } !a ==> v4.choose(a, b, c) == c);
+
+axiom (forall a: bool :: { v4.LIFT(a) } a <==> v4.LIFT(a) != 0);
+
+axiom (forall a: int :: { v4.PTR_NOT(a) } a == 0 ==> v4.PTR_NOT(a) != 0);
+
+axiom (forall a: int :: { v4.PTR_NOT(a) } a != 0 ==> v4.PTR_NOT(a) == 0);
+
+axiom (forall a: int :: { v4.NULL_CHECK(a) } a == 0 ==> v4.NULL_CHECK(a) != 0);
+
+axiom (forall a: int :: { v4.NULL_CHECK(a) } a != 0 ==> v4.NULL_CHECK(a) == 0);
+
+axiom (forall n: int, x: int, y: int :: { v4.AtLeast(n, x)[y] } v4.AtLeast(n, x)[y] ==> v4.INT_LEQ(x, y) && v4.Rep(n, x) == v4.Rep(n, y));
+
+axiom (forall n: int, x: int, y: int :: { v4.AtLeast(n, x), v4.Rep(n, x), v4.Rep(n, y) } v4.INT_LEQ(x, y) && v4.Rep(n, x) == v4.Rep(n, y) ==> v4.AtLeast(n, x)[y]);
+
+axiom (forall n: int, x: int :: { v4.AtLeast(n, x) } v4.AtLeast(n, x)[x]);
+
+axiom (forall n: int, x: int, z: int :: { v4.PLUS(x, n, z) } v4.Rep(n, x) == v4.Rep(n, v4.PLUS(x, n, z)));
+
+axiom (forall n: int, x: int :: { v4.Rep(n, x) } (exists k: int :: v4.INT_SUB(v4.Rep(n, x), x) == v4.INT_MULT(n, k)));
+
+axiom (forall x: int, n: int, z: int :: { v4.Array(x, n, z) } v4.INT_LEQ(z, 0) ==> v4.Equal(v4.Array(x, n, z), v4.Empty()));
+
+axiom (forall x: int, n: int, z: int :: { v4.Array(x, n, z) } v4.INT_GT(z, 0) ==> v4.Equal(v4.Array(x, n, z), v4.Difference(v4.AtLeast(n, x), v4.AtLeast(n, v4.PLUS(x, n, z)))));
+
+axiom (forall x: int :: !v4.Empty()[x]);
+
+axiom (forall x: int :: v4.SetTrue()[x]);
+
+axiom (forall x: int, y: int :: { v4.Singleton(y)[x] } v4.Singleton(y)[x] <==> x == y);
+
+axiom (forall y: int :: { v4.Singleton(y) } v4.Singleton(y)[y]);
+
+axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Union(S, T)[x] } { v4.Union(S, T), S[x] } { v4.Union(S, T), T[x] } v4.Union(S, T)[x] <==> S[x] || T[x]);
+
+axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Intersection(S, T)[x] } { v4.Intersection(S, T), S[x] } { v4.Intersection(S, T), T[x] } v4.Intersection(S, T)[x] <==> S[x] && T[x]);
+
+axiom (forall x: int, S: [int]bool, T: [int]bool :: { v4.Difference(S, T)[x] } { v4.Difference(S, T), S[x] } { v4.Difference(S, T), T[x] } v4.Difference(S, T)[x] <==> S[x] && !T[x]);
+
+axiom (forall S: [int]bool, T: [int]bool :: { v4.Equal(S, T) } v4.Equal(S, T) <==> v4.Subset(S, T) && v4.Subset(T, S));
+
+axiom (forall x: int, S: [int]bool, T: [int]bool :: { S[x], v4.Subset(S, T) } { T[x], v4.Subset(S, T) } S[x] && v4.Subset(S, T) ==> T[x]);
+
+axiom (forall S: [int]bool, T: [int]bool :: { v4.Subset(S, T) } v4.Subset(S, T) || (exists x: int :: S[x] && !T[x]));
+
+axiom (forall x: int, S: [int]bool, T: [int]bool :: { S[x], v4.Disjoint(S, T) } { T[x], v4.Disjoint(S, T) } !(S[x] && v4.Disjoint(S, T) && T[x]));
+
+axiom (forall S: [int]bool, T: [int]bool :: { v4.Disjoint(S, T) } v4.Disjoint(S, T) || (exists x: int :: S[x] && T[x]));
+
+axiom (forall f: [int]int, x: int :: { v4.Inverse(f, f[x]) } v4.Inverse(f, f[x])[x]);
+
+axiom (forall f: [int]int, x: int, y: int :: { v4.Inverse(f, y), f[x] } v4.Inverse(f, y)[x] ==> f[x] == y);
+
+axiom (forall f: [int]int, x: int, y: int :: { v4.Inverse(f[x := y], y) } v4.Equal(v4.Inverse(f[x := y], y), v4.Union(v4.Inverse(f, y), v4.Singleton(x))));
+
+axiom (forall f: [int]int, x: int, y: int, z: int :: { v4.Inverse(f[x := y], z) } y == z || v4.Equal(v4.Inverse(f[x := y], z), v4.Difference(v4.Inverse(f, z), v4.Singleton(x))));
+
+axiom (forall x: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M)[x] } v4.Dereference(S, M)[x] ==> (exists y: int :: x == M[y] && S[y]));
+
+axiom (forall x: int, S: [int]bool, M: [int]int :: { M[x], S[x], v4.Dereference(S, M) } S[x] ==> v4.Dereference(S, M)[M[x]]);
+
+axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } !S[x] ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Dereference(S, M)));
+
+axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } S[x] && v4.Equal(v4.Intersection(v4.Inverse(M, M[x]), S), v4.Singleton(x)) ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Union(v4.Difference(v4.Dereference(S, M), v4.Singleton(M[x])), v4.Singleton(y))));
+
+axiom (forall x: int, y: int, S: [int]bool, M: [int]int :: { v4.Dereference(S, M[x := y]) } S[x] && !v4.Equal(v4.Intersection(v4.Inverse(M, M[x]), S), v4.Singleton(x)) ==> v4.Equal(v4.Dereference(S, M[x := y]), v4.Union(v4.Dereference(S, M), v4.Singleton(y))));
+
+axiom (forall M: [name][int]int, x: int :: { v4.Unified(M)[x] } v4.Unified(M)[x] == M[v4.Field(x)][x]);
+
+axiom (forall M: [name][int]int, x: int, y: int :: { v4.Unified(M[v4.Field(x) := M[v4.Field(x)][x := y]]) } v4.Unified(M[v4.Field(x) := M[v4.Field(x)][x := y]]) == v4.Unified(M)[x := y]);
+
+procedure v2.havoc_assert(i: int);
+
+
+
+procedure v2.havoc_assume(i: int);
+
+
+
+procedure v2.__HAVOC_free(a: int);
+
+
+
+procedure v2.__HAVOC_malloc(obj_size: int) returns (new: int);
+ free ensures new == _uf_v4.__HAVOC_malloc_new(obj_size);
+
+
+
+procedure v2.__HAVOC_det_malloc(obj_size: int) returns (new: int);
+ free ensures new == _uf_v4.__HAVOC_det_malloc_new(obj_size);
+
+
+
+procedure v2.__HAVOC_memset_split_1(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int);
+ free ensures ret == _uf_v4.__HAVOC_memset_split_1_ret(A, p, c, n);
+
+
+
+procedure v2.__HAVOC_memset_split_2(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int);
+ free ensures ret == _uf_v4.__HAVOC_memset_split_2_ret(A, p, c, n);
+
+
+
+procedure v2.__HAVOC_memset_split_4(A: [int]int, p: int, c: int, n: int) returns (ret: [int]int);
+ free ensures ret == _uf_v4.__HAVOC_memset_split_4_ret(A, p, c, n);
+
+
+
+procedure v2.nondet_choice() returns (x: int);
+ free ensures x == _uf_v4.nondet_choice_x();
+
+
+
+procedure v2.det_choice() returns (x: int);
+ free ensures x == _uf_v4.det_choice_x();
+
+
+
+procedure v2._strdup(str: int) returns (new: int);
+ free ensures new == _uf_v4._strdup_new(str);
+
+
+
+procedure v2._xstrcasecmp(a0: int, a1: int) returns (ret: int);
+ free ensures ret == _uf_v4._xstrcasecmp_ret(a0, a1);
+
+
+
+procedure v2._xstrcmp(a0: int, a1: int) returns (ret: int);
+ free ensures ret == _uf_v4._xstrcmp_ret(a0, a1);
+
+
+
+procedure {:inline 1} v2.Eval(e_.1: int);
+ modifies v4.Mem_T.result__EXPR;
+ free ensures v4.Mem_T.result__EXPR == _uf_v4.Eval_v4.Mem_T.result__EXPR(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned));
+
+
+
+procedure v2.EvalEntry1(e_.1: int, outval_.1: int);
+ modifies v4.Mem_T.result__EXPR, v4.Mem_T.INT4;
+ free ensures v4.Mem_T.result__EXPR == _uf_v4.EvalEntry1_v4.Mem_T.result__EXPR(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned));
+ free ensures v4.Mem_T.INT4 == _uf_v4.EvalEntry1_v4.Mem_T.INT4(e_.1, outval_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.Mem_T.INT4), old(v4.isUnsigned));
+
+
+
+procedure v2.EvalEntry2(e_.1: int);
+ modifies v4.Mem_T.result__EXPR;
+ free ensures v4.Mem_T.result__EXPR == _uf_v4.EvalEntry2_v4.Mem_T.result__EXPR(e_.1, old(v4.alloc), old(v4.Mem_T.oper__EXPR), old(v4.Mem_T.op1__EXPR), old(v4.Mem_T.op2__EXPR), old(v4.Mem_T.result__EXPR), old(v4.isUnsigned));
+
+
+
+procedure v2.__havoc_heapglobal_init();
+
+
+
+implementation {:inline 1} v2.Eval(e_.1: int)
+{
+ var havoc_stringTemp: int;
+ var condVal: int;
+ var a1: int;
+ var a2: int;
+ var e: int;
+ var op: int;
+ var res: int;
+ var tempBoogie0: int;
+ var tempBoogie1: int;
+ var tempBoogie2: int;
+ var tempBoogie3: int;
+ var tempBoogie4: int;
+ var tempBoogie5: int;
+ var tempBoogie6: int;
+ var tempBoogie7: int;
+ var tempBoogie8: int;
+ var tempBoogie9: int;
+ var tempBoogie10: int;
+ var tempBoogie11: int;
+ var tempBoogie12: int;
+ var tempBoogie13: int;
+ var tempBoogie14: int;
+ var tempBoogie15: int;
+ var tempBoogie16: int;
+ var tempBoogie17: int;
+ var tempBoogie18: int;
+ var tempBoogie19: int;
+ var __havoc_dummy_return: int;
+
+ anon0#2:
+ havoc_stringTemp := 0;
+ goto start#2;
+
+ start#2:
+ assume v4.INT_LT(e_.1, v4.alloc);
+ a1 := 0;
+ a2 := 0;
+ e := 0;
+ op := 0;
+ res := 0;
+ e := e_.1;
+ goto label_3#2;
+
+ label_3#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true;
+ goto label_4#2;
+
+ label_4#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true;
+ goto label_5#2;
+
+ label_5#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true;
+ goto label_6#2;
+
+ label_6#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true;
+ goto label_7#2;
+
+ label_7#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 19} true;
+ assert true;
+ op := v4.Mem_T.oper__EXPR[v4.oper__EXPR(e)];
+ assume v4.value_is(v2.__ctobpl_const_1, op);
+ assume v4.value_is(v2.__ctobpl_const_2, e);
+ assume v4.value_is(v2.__ctobpl_const_3, v4.Mem_T.oper__EXPR[v4.oper__EXPR(e)]);
+ goto label_8#2;
+
+ label_8#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 20} true;
+ assert true;
+ a1 := v4.Mem_T.op1__EXPR[v4.op1__EXPR(e)];
+ assume v4.value_is(v2.__ctobpl_const_4, a1);
+ assume v4.value_is(v2.__ctobpl_const_5, e);
+ assume v4.value_is(v2.__ctobpl_const_6, v4.Mem_T.op1__EXPR[v4.op1__EXPR(e)]);
+ goto label_9#2;
+
+ label_9#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 21} true;
+ assert true;
+ a2 := v4.Mem_T.op2__EXPR[v4.op2__EXPR(e)];
+ assume v4.value_is(v2.__ctobpl_const_7, a2);
+ assume v4.value_is(v2.__ctobpl_const_8, e);
+ assume v4.value_is(v2.__ctobpl_const_9, v4.Mem_T.op2__EXPR[v4.op2__EXPR(e)]);
+ goto label_10#2;
+
+ label_10#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 22} true;
+ res := 0 - 1;
+ assume v4.value_is(v2.__ctobpl_const_10, res);
+ goto label_11#2;
+
+ label_11#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 24} true;
+ goto label_11_case_0#2, label_11_case_1#2, label_11_case_2#2;
+
+ label_11_case_2#2:
+ assume v4.INT_EQ(op, 2);
+ assume v4.value_is(v2.__ctobpl_const_11, op);
+ goto label_14#2;
+
+ label_14#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 29} true;
+ res := v4.MINUS_BOTH_PTR_OR_BOTH_INT(a1, a2, 1);
+ assume v4.value_is(v2.__ctobpl_const_18, res);
+ assume v4.value_is(v2.__ctobpl_const_19, a1);
+ assume v4.value_is(v2.__ctobpl_const_20, a2);
+ goto label_12#2;
+
+ label_11_case_1#2:
+ assume v4.INT_EQ(op, 1);
+ assume v4.value_is(v2.__ctobpl_const_11, op);
+ goto label_13#2;
+
+ label_13#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 27} true;
+ res := v4.PLUS(a1, 1, a2);
+ assume v4.value_is(v2.__ctobpl_const_15, res);
+ assume v4.value_is(v2.__ctobpl_const_16, a1);
+ assume v4.value_is(v2.__ctobpl_const_17, a2);
+ goto label_12#2;
+
+ label_11_case_0#2:
+ assume v4.INT_NEQ(op, 1);
+ assume v4.INT_NEQ(op, 2);
+ assume v4.value_is(v2.__ctobpl_const_11, op);
+ goto label_12#2;
+
+ label_12#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 35} true;
+ assert true;
+ v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR[v4.result__EXPR(e) := res];
+ assume v4.value_is(v2.__ctobpl_const_12, e);
+ assume v4.value_is(v2.__ctobpl_const_13, v4.Mem_T.result__EXPR[v4.result__EXPR(e)]);
+ assume v4.value_is(v2.__ctobpl_const_14, res);
+ goto label_1#2;
+
+ label_1#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 36} true;
+ return;
+}
+
+
+
+implementation v2.EvalEntry1(e_.1: int, outval_.1: int)
+{
+ var havoc_stringTemp: int;
+ var condVal: int;
+ var e: int;
+ var outval: int;
+ var tempBoogie0: int;
+ var tempBoogie1: int;
+ var tempBoogie2: int;
+ var tempBoogie3: int;
+ var tempBoogie4: int;
+ var tempBoogie5: int;
+ var tempBoogie6: int;
+ var tempBoogie7: int;
+ var tempBoogie8: int;
+ var tempBoogie9: int;
+ var tempBoogie10: int;
+ var tempBoogie11: int;
+ var tempBoogie12: int;
+ var tempBoogie13: int;
+ var tempBoogie14: int;
+ var tempBoogie15: int;
+ var tempBoogie16: int;
+ var tempBoogie17: int;
+ var tempBoogie18: int;
+ var tempBoogie19: int;
+ var __havoc_dummy_return: int;
+
+ anon0#2:
+ havoc_stringTemp := 0;
+ goto start#2;
+
+ start#2:
+ assume v4.INT_LT(e_.1, v4.alloc);
+ assume v4.INT_LT(outval_.1, v4.alloc);
+ e := 0;
+ outval := 0;
+ e := e_.1;
+ outval := outval_.1;
+ goto label_3#2;
+
+ label_3#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 40} true;
+ call v2.Eval(e);
+ assume v4.value_is(v2.__ctobpl_const_21, e);
+ assume v4.value_is(v2.__ctobpl_const_22, e);
+ goto label_6#2;
+
+ label_6#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 41} true;
+ assert true;
+ assert true;
+ v4.Mem_T.INT4 := v4.Mem_T.INT4[outval := v4.Mem_T.result__EXPR[v4.result__EXPR(e)]];
+ assume v4.value_is(v2.__ctobpl_const_23, outval);
+ assume v4.value_is(v2.__ctobpl_const_24, v4.Mem_T.INT4[outval]);
+ assume v4.value_is(v2.__ctobpl_const_25, e);
+ assume v4.value_is(v2.__ctobpl_const_26, v4.Mem_T.result__EXPR[v4.result__EXPR(e)]);
+ goto label_1#2;
+
+ label_1#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 42} true;
+ return;
+}
+
+
+
+implementation v2.EvalEntry2(e_.1: int)
+{
+ var havoc_stringTemp: int;
+ var condVal: int;
+ var e: int;
+ var tempBoogie0: int;
+ var tempBoogie1: int;
+ var tempBoogie2: int;
+ var tempBoogie3: int;
+ var tempBoogie4: int;
+ var tempBoogie5: int;
+ var tempBoogie6: int;
+ var tempBoogie7: int;
+ var tempBoogie8: int;
+ var tempBoogie9: int;
+ var tempBoogie10: int;
+ var tempBoogie11: int;
+ var tempBoogie12: int;
+ var tempBoogie13: int;
+ var tempBoogie14: int;
+ var tempBoogie15: int;
+ var tempBoogie16: int;
+ var tempBoogie17: int;
+ var tempBoogie18: int;
+ var tempBoogie19: int;
+ var __havoc_dummy_return: int;
+
+ anon0#2:
+ havoc_stringTemp := 0;
+ goto start#2;
+
+ start#2:
+ assume v4.INT_LT(e_.1, v4.alloc);
+ e := 0;
+ e := e_.1;
+ goto label_3#2;
+
+ label_3#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 46} true;
+ call v2.Eval(e);
+ assume v4.value_is(v2.__ctobpl_const_27, e);
+ assume v4.value_is(v2.__ctobpl_const_28, e);
+ goto label_1#2;
+
+ label_1#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 47} true;
+ return;
+}
+
+
+
+implementation v2.__havoc_heapglobal_init()
+{
+
+ anon0#2:
+ return;
+}
+
+
+
+type name;
+
+type byte;
+
+var Output_of_v2.Eval_v4.Mem_T.result__EXPR: [int]int;
+
+var Output_of_v4.Eval_v4.Mem_T.result__EXPR: [int]int;
+
+procedure EQ_v2.Eval__v4.Eval(e_.1: int) returns (AA_TEMP30: bool);
+ modifies v4.Mem_T.result__EXPR, Output_of_v2.Eval_v4.Mem_T.result__EXPR, Output_of_v4.Eval_v4.Mem_T.result__EXPR;
+ ensures AA_TEMP30;
+
+
+
+implementation EQ_v2.Eval__v4.Eval(e_.1: int) returns (AA_TEMP30: bool)
+{
+ var AA_TEMP10: [int]int;
+ var AA_TEMP00: [int]int;
+ var inline$v2.Eval$0$havoc_stringTemp: int;
+ var inline$v2.Eval$0$condVal: int;
+ var inline$v2.Eval$0$a1: int;
+ var inline$v2.Eval$0$a2: int;
+ var inline$v2.Eval$0$e: int;
+ var inline$v2.Eval$0$op: int;
+ var inline$v2.Eval$0$res: int;
+ var inline$v2.Eval$0$tempBoogie0: int;
+ var inline$v2.Eval$0$tempBoogie1: int;
+ var inline$v2.Eval$0$tempBoogie2: int;
+ var inline$v2.Eval$0$tempBoogie3: int;
+ var inline$v2.Eval$0$tempBoogie4: int;
+ var inline$v2.Eval$0$tempBoogie5: int;
+ var inline$v2.Eval$0$tempBoogie6: int;
+ var inline$v2.Eval$0$tempBoogie7: int;
+ var inline$v2.Eval$0$tempBoogie8: int;
+ var inline$v2.Eval$0$tempBoogie9: int;
+ var inline$v2.Eval$0$tempBoogie10: int;
+ var inline$v2.Eval$0$tempBoogie11: int;
+ var inline$v2.Eval$0$tempBoogie12: int;
+ var inline$v2.Eval$0$tempBoogie13: int;
+ var inline$v2.Eval$0$tempBoogie14: int;
+ var inline$v2.Eval$0$tempBoogie15: int;
+ var inline$v2.Eval$0$tempBoogie16: int;
+ var inline$v2.Eval$0$tempBoogie17: int;
+ var inline$v2.Eval$0$tempBoogie18: int;
+ var inline$v2.Eval$0$tempBoogie19: int;
+ var inline$v2.Eval$0$__havoc_dummy_return: int;
+ var inline$v2.Eval$0$e_.1: int;
+ var inline$v2.Eval$0$v4.Mem_T.result__EXPR: [int]int;
+ var inline$v4.Eval$0$havoc_stringTemp: int;
+ var inline$v4.Eval$0$condVal: int;
+ var inline$v4.Eval$0$a1: int;
+ var inline$v4.Eval$0$a2: int;
+ var inline$v4.Eval$0$e: int;
+ var inline$v4.Eval$0$op: int;
+ var inline$v4.Eval$0$res: int;
+ var inline$v4.Eval$0$result.UnsignedAdd$1: int;
+ var inline$v4.Eval$0$result.UnsignedSub$2: int;
+ var inline$v4.Eval$0$tempBoogie0: int;
+ var inline$v4.Eval$0$tempBoogie1: int;
+ var inline$v4.Eval$0$tempBoogie2: int;
+ var inline$v4.Eval$0$tempBoogie3: int;
+ var inline$v4.Eval$0$tempBoogie4: int;
+ var inline$v4.Eval$0$tempBoogie5: int;
+ var inline$v4.Eval$0$tempBoogie6: int;
+ var inline$v4.Eval$0$tempBoogie7: int;
+ var inline$v4.Eval$0$tempBoogie8: int;
+ var inline$v4.Eval$0$tempBoogie9: int;
+ var inline$v4.Eval$0$tempBoogie10: int;
+ var inline$v4.Eval$0$tempBoogie11: int;
+ var inline$v4.Eval$0$tempBoogie12: int;
+ var inline$v4.Eval$0$tempBoogie13: int;
+ var inline$v4.Eval$0$tempBoogie14: int;
+ var inline$v4.Eval$0$tempBoogie15: int;
+ var inline$v4.Eval$0$tempBoogie16: int;
+ var inline$v4.Eval$0$tempBoogie17: int;
+ var inline$v4.Eval$0$tempBoogie18: int;
+ var inline$v4.Eval$0$tempBoogie19: int;
+ var inline$v4.Eval$0$__havoc_dummy_return: int;
+ var inline$v4.Eval$0$e_.1: int;
+ var inline$v4.Eval$0$v4.Mem_T.result__EXPR: [int]int;
+
+ AA_INSTR_EQ_BODY:
+ AA_TEMP00 := v4.Mem_T.result__EXPR;
+ goto inline$v2.Eval$0$Entry;
+
+ inline$v2.Eval$0$Entry:
+ inline$v2.Eval$0$e_.1 := e_.1;
+ inline$v2.Eval$0$v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR;
+ goto inline$v2.Eval$0$anon0#2;
+
+ inline$v2.Eval$0$anon0#2:
+ inline$v2.Eval$0$havoc_stringTemp := 0;
+ goto inline$v2.Eval$0$start#2;
+
+ inline$v2.Eval$0$start#2:
+ assume v4.INT_LT(inline$v2.Eval$0$e_.1, v4.alloc);
+ inline$v2.Eval$0$a1 := 0;
+ inline$v2.Eval$0$a2 := 0;
+ inline$v2.Eval$0$e := 0;
+ inline$v2.Eval$0$op := 0;
+ inline$v2.Eval$0$res := 0;
+ inline$v2.Eval$0$e := inline$v2.Eval$0$e_.1;
+ goto inline$v2.Eval$0$label_3#2;
+
+ inline$v2.Eval$0$label_3#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true;
+ goto inline$v2.Eval$0$label_4#2;
+
+ inline$v2.Eval$0$label_4#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true;
+ goto inline$v2.Eval$0$label_5#2;
+
+ inline$v2.Eval$0$label_5#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true;
+ goto inline$v2.Eval$0$label_6#2;
+
+ inline$v2.Eval$0$label_6#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 17} true;
+ goto inline$v2.Eval$0$label_7#2;
+
+ inline$v2.Eval$0$label_7#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 19} true;
+ assert true;
+ inline$v2.Eval$0$op := v4.Mem_T.oper__EXPR[v4.oper__EXPR(inline$v2.Eval$0$e)];
+ assume v4.value_is(v2.__ctobpl_const_1, inline$v2.Eval$0$op);
+ assume v4.value_is(v2.__ctobpl_const_2, inline$v2.Eval$0$e);
+ assume v4.value_is(v2.__ctobpl_const_3, v4.Mem_T.oper__EXPR[v4.oper__EXPR(inline$v2.Eval$0$e)]);
+ goto inline$v2.Eval$0$label_8#2;
+
+ inline$v2.Eval$0$label_8#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 20} true;
+ assert true;
+ inline$v2.Eval$0$a1 := v4.Mem_T.op1__EXPR[v4.op1__EXPR(inline$v2.Eval$0$e)];
+ assume v4.value_is(v2.__ctobpl_const_4, inline$v2.Eval$0$a1);
+ assume v4.value_is(v2.__ctobpl_const_5, inline$v2.Eval$0$e);
+ assume v4.value_is(v2.__ctobpl_const_6, v4.Mem_T.op1__EXPR[v4.op1__EXPR(inline$v2.Eval$0$e)]);
+ goto inline$v2.Eval$0$label_9#2;
+
+ inline$v2.Eval$0$label_9#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 21} true;
+ assert true;
+ inline$v2.Eval$0$a2 := v4.Mem_T.op2__EXPR[v4.op2__EXPR(inline$v2.Eval$0$e)];
+ assume v4.value_is(v2.__ctobpl_const_7, inline$v2.Eval$0$a2);
+ assume v4.value_is(v2.__ctobpl_const_8, inline$v2.Eval$0$e);
+ assume v4.value_is(v2.__ctobpl_const_9, v4.Mem_T.op2__EXPR[v4.op2__EXPR(inline$v2.Eval$0$e)]);
+ goto inline$v2.Eval$0$label_10#2;
+
+ inline$v2.Eval$0$label_10#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 22} true;
+ inline$v2.Eval$0$res := 0 - 1;
+ assume v4.value_is(v2.__ctobpl_const_10, inline$v2.Eval$0$res);
+ goto inline$v2.Eval$0$label_11#2;
+
+ inline$v2.Eval$0$label_11#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 24} true;
+ goto inline$v2.Eval$0$label_11_case_0#2, inline$v2.Eval$0$label_11_case_1#2, inline$v2.Eval$0$label_11_case_2#2;
+
+ inline$v2.Eval$0$label_11_case_2#2:
+ assume v4.INT_EQ(inline$v2.Eval$0$op, 2);
+ assume v4.value_is(v2.__ctobpl_const_11, inline$v2.Eval$0$op);
+ goto inline$v2.Eval$0$label_14#2;
+
+ inline$v2.Eval$0$label_14#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 29} true;
+ inline$v2.Eval$0$res := v4.MINUS_BOTH_PTR_OR_BOTH_INT(inline$v2.Eval$0$a1, inline$v2.Eval$0$a2, 1);
+ assume v4.value_is(v2.__ctobpl_const_18, inline$v2.Eval$0$res);
+ assume v4.value_is(v2.__ctobpl_const_19, inline$v2.Eval$0$a1);
+ assume v4.value_is(v2.__ctobpl_const_20, inline$v2.Eval$0$a2);
+ goto inline$v2.Eval$0$label_12#2;
+
+ inline$v2.Eval$0$label_11_case_1#2:
+ assume v4.INT_EQ(inline$v2.Eval$0$op, 1);
+ assume v4.value_is(v2.__ctobpl_const_11, inline$v2.Eval$0$op);
+ goto inline$v2.Eval$0$label_13#2;
+
+ inline$v2.Eval$0$label_13#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 27} true;
+ inline$v2.Eval$0$res := v4.PLUS(inline$v2.Eval$0$a1, 1, inline$v2.Eval$0$a2);
+ assume v4.value_is(v2.__ctobpl_const_15, inline$v2.Eval$0$res);
+ assume v4.value_is(v2.__ctobpl_const_16, inline$v2.Eval$0$a1);
+ assume v4.value_is(v2.__ctobpl_const_17, inline$v2.Eval$0$a2);
+ goto inline$v2.Eval$0$label_12#2;
+
+ inline$v2.Eval$0$label_11_case_0#2:
+ assume v4.INT_NEQ(inline$v2.Eval$0$op, 1);
+ assume v4.INT_NEQ(inline$v2.Eval$0$op, 2);
+ assume v4.value_is(v2.__ctobpl_const_11, inline$v2.Eval$0$op);
+ goto inline$v2.Eval$0$label_12#2;
+
+ inline$v2.Eval$0$label_12#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 35} true;
+ assert true;
+ v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR[v4.result__EXPR(inline$v2.Eval$0$e) := inline$v2.Eval$0$res];
+ assume v4.value_is(v2.__ctobpl_const_12, inline$v2.Eval$0$e);
+ assume v4.value_is(v2.__ctobpl_const_13, v4.Mem_T.result__EXPR[v4.result__EXPR(inline$v2.Eval$0$e)]);
+ assume v4.value_is(v2.__ctobpl_const_14, inline$v2.Eval$0$res);
+ goto inline$v2.Eval$0$label_1#2;
+
+ inline$v2.Eval$0$label_1#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v2\foo.c"} {:sourceline 36} true;
+ goto inline$v2.Eval$0$Return;
+
+ inline$v2.Eval$0$Return:
+ goto AA_INSTR_EQ_BODY$1;
+
+ AA_INSTR_EQ_BODY$1:
+ AA_TEMP10 := v4.Mem_T.result__EXPR;
+ v4.Mem_T.result__EXPR := AA_TEMP00;
+ goto inline$v4.Eval$0$Entry;
+
+ inline$v4.Eval$0$Entry:
+ inline$v4.Eval$0$e_.1 := e_.1;
+ inline$v4.Eval$0$v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR;
+ goto inline$v4.Eval$0$anon0#2;
+
+ inline$v4.Eval$0$anon0#2:
+ inline$v4.Eval$0$havoc_stringTemp := 0;
+ goto inline$v4.Eval$0$start#2;
+
+ inline$v4.Eval$0$start#2:
+ assume v4.INT_LT(inline$v4.Eval$0$e_.1, v4.alloc);
+ inline$v4.Eval$0$a1 := 0;
+ inline$v4.Eval$0$a2 := 0;
+ inline$v4.Eval$0$e := 0;
+ inline$v4.Eval$0$op := 0;
+ inline$v4.Eval$0$res := 0;
+ inline$v4.Eval$0$result.UnsignedAdd$1 := 0;
+ inline$v4.Eval$0$result.UnsignedSub$2 := 0;
+ inline$v4.Eval$0$e := inline$v4.Eval$0$e_.1;
+ goto inline$v4.Eval$0$label_3#2;
+
+ inline$v4.Eval$0$label_3#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true;
+ goto inline$v4.Eval$0$label_4#2;
+
+ inline$v4.Eval$0$label_4#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true;
+ goto inline$v4.Eval$0$label_5#2;
+
+ inline$v4.Eval$0$label_5#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true;
+ goto inline$v4.Eval$0$label_6#2;
+
+ inline$v4.Eval$0$label_6#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 19} true;
+ goto inline$v4.Eval$0$label_7#2;
+
+ inline$v4.Eval$0$label_7#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 21} true;
+ assert true;
+ inline$v4.Eval$0$op := v4.Mem_T.oper__EXPR[v4.oper__EXPR(inline$v4.Eval$0$e)];
+ assume v4.value_is(v4.__ctobpl_const_1, inline$v4.Eval$0$op);
+ assume v4.value_is(v4.__ctobpl_const_2, inline$v4.Eval$0$e);
+ assume v4.value_is(v4.__ctobpl_const_3, v4.Mem_T.oper__EXPR[v4.oper__EXPR(inline$v4.Eval$0$e)]);
+ goto inline$v4.Eval$0$label_8#2;
+
+ inline$v4.Eval$0$label_8#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 22} true;
+ assert true;
+ inline$v4.Eval$0$a1 := v4.Mem_T.op1__EXPR[v4.op1__EXPR(inline$v4.Eval$0$e)];
+ assume v4.value_is(v4.__ctobpl_const_4, inline$v4.Eval$0$a1);
+ assume v4.value_is(v4.__ctobpl_const_5, inline$v4.Eval$0$e);
+ assume v4.value_is(v4.__ctobpl_const_6, v4.Mem_T.op1__EXPR[v4.op1__EXPR(inline$v4.Eval$0$e)]);
+ goto inline$v4.Eval$0$label_9#2;
+
+ inline$v4.Eval$0$label_9#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 23} true;
+ assert true;
+ inline$v4.Eval$0$a2 := v4.Mem_T.op2__EXPR[v4.op2__EXPR(inline$v4.Eval$0$e)];
+ assume v4.value_is(v4.__ctobpl_const_7, inline$v4.Eval$0$a2);
+ assume v4.value_is(v4.__ctobpl_const_8, inline$v4.Eval$0$e);
+ assume v4.value_is(v4.__ctobpl_const_9, v4.Mem_T.op2__EXPR[v4.op2__EXPR(inline$v4.Eval$0$e)]);
+ goto inline$v4.Eval$0$label_10#2;
+
+ inline$v4.Eval$0$label_10#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 24} true;
+ inline$v4.Eval$0$res := 0 - 1;
+ assume v4.value_is(v4.__ctobpl_const_10, inline$v4.Eval$0$res);
+ goto inline$v4.Eval$0$label_11#2;
+
+ inline$v4.Eval$0$label_11#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 26} true;
+ goto inline$v4.Eval$0$label_11_case_0#2, inline$v4.Eval$0$label_11_case_1#2, inline$v4.Eval$0$label_11_case_2#2;
+
+ inline$v4.Eval$0$label_11_case_2#2:
+ assume v4.INT_EQ(inline$v4.Eval$0$op, 2);
+ assume v4.value_is(v4.__ctobpl_const_11, inline$v4.Eval$0$op);
+ goto inline$v4.Eval$0$label_14#2;
+
+ inline$v4.Eval$0$label_14#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 35} true;
+ goto inline$v4.Eval$0$label_14_true#2, inline$v4.Eval$0$label_14_false#2;
+
+ inline$v4.Eval$0$label_14_false#2:
+ assume v4.isUnsigned == 0;
+ assume v4.value_is(v4.__ctobpl_const_16, v4.isUnsigned);
+ goto inline$v4.Eval$0$label_15#2;
+
+ inline$v4.Eval$0$label_15#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 38} true;
+ inline$v4.Eval$0$res := v4.MINUS_BOTH_PTR_OR_BOTH_INT(inline$v4.Eval$0$a1, inline$v4.Eval$0$a2, 1);
+ assume v4.value_is(v4.__ctobpl_const_17, inline$v4.Eval$0$res);
+ assume v4.value_is(v4.__ctobpl_const_18, inline$v4.Eval$0$a1);
+ assume v4.value_is(v4.__ctobpl_const_19, inline$v4.Eval$0$a2);
+ goto inline$v4.Eval$0$label_12#2;
+
+ inline$v4.Eval$0$label_14_true#2:
+ assume v4.isUnsigned != 0;
+ assume v4.value_is(v4.__ctobpl_const_16, v4.isUnsigned);
+ goto inline$v4.Eval$0$label_16#2;
+
+ inline$v4.Eval$0$label_16#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 36} true;
+ call inline$v4.Eval$0$result.UnsignedSub$2 := v4.UnsignedSub(inline$v4.Eval$0$a1, inline$v4.Eval$0$a2);
+ assume v4.value_is(v4.__ctobpl_const_20, inline$v4.Eval$0$a1);
+ assume v4.value_is(v4.__ctobpl_const_21, inline$v4.Eval$0$a2);
+ assume v4.value_is(v4.__ctobpl_const_22, inline$v4.Eval$0$a1);
+ assume v4.value_is(v4.__ctobpl_const_23, inline$v4.Eval$0$a2);
+ goto inline$v4.Eval$0$label_19#2;
+
+ inline$v4.Eval$0$label_19#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 36} true;
+ inline$v4.Eval$0$res := inline$v4.Eval$0$result.UnsignedSub$2;
+ assume v4.value_is(v4.__ctobpl_const_24, inline$v4.Eval$0$res);
+ assume v4.value_is(v4.__ctobpl_const_25, inline$v4.Eval$0$result.UnsignedSub$2);
+ goto inline$v4.Eval$0$label_12#2;
+
+ inline$v4.Eval$0$label_11_case_1#2:
+ assume v4.INT_EQ(inline$v4.Eval$0$op, 1);
+ assume v4.value_is(v4.__ctobpl_const_11, inline$v4.Eval$0$op);
+ goto inline$v4.Eval$0$label_13#2;
+
+ inline$v4.Eval$0$label_13#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 29} true;
+ goto inline$v4.Eval$0$label_13_true#2, inline$v4.Eval$0$label_13_false#2;
+
+ inline$v4.Eval$0$label_13_false#2:
+ assume v4.isUnsigned == 0;
+ assume v4.value_is(v4.__ctobpl_const_15, v4.isUnsigned);
+ goto inline$v4.Eval$0$label_20#2;
+
+ inline$v4.Eval$0$label_20#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 32} true;
+ inline$v4.Eval$0$res := v4.PLUS(inline$v4.Eval$0$a1, 1, inline$v4.Eval$0$a2);
+ assume v4.value_is(v4.__ctobpl_const_26, inline$v4.Eval$0$res);
+ assume v4.value_is(v4.__ctobpl_const_27, inline$v4.Eval$0$a1);
+ assume v4.value_is(v4.__ctobpl_const_28, inline$v4.Eval$0$a2);
+ goto inline$v4.Eval$0$label_12#2;
+
+ inline$v4.Eval$0$label_13_true#2:
+ assume v4.isUnsigned != 0;
+ assume v4.value_is(v4.__ctobpl_const_15, v4.isUnsigned);
+ goto inline$v4.Eval$0$label_21#2;
+
+ inline$v4.Eval$0$label_21#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 30} true;
+ call inline$v4.Eval$0$result.UnsignedAdd$1 := v4.UnsignedAdd(inline$v4.Eval$0$a1, inline$v4.Eval$0$a2);
+ assume v4.value_is(v4.__ctobpl_const_29, inline$v4.Eval$0$a1);
+ assume v4.value_is(v4.__ctobpl_const_30, inline$v4.Eval$0$a2);
+ assume v4.value_is(v4.__ctobpl_const_31, inline$v4.Eval$0$a1);
+ assume v4.value_is(v4.__ctobpl_const_32, inline$v4.Eval$0$a2);
+ goto inline$v4.Eval$0$label_24#2;
+
+ inline$v4.Eval$0$label_24#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 30} true;
+ inline$v4.Eval$0$res := inline$v4.Eval$0$result.UnsignedAdd$1;
+ assume v4.value_is(v4.__ctobpl_const_33, inline$v4.Eval$0$res);
+ assume v4.value_is(v4.__ctobpl_const_34, inline$v4.Eval$0$result.UnsignedAdd$1);
+ goto inline$v4.Eval$0$label_12#2;
+
+ inline$v4.Eval$0$label_11_case_0#2:
+ assume v4.INT_NEQ(inline$v4.Eval$0$op, 1);
+ assume v4.INT_NEQ(inline$v4.Eval$0$op, 2);
+ assume v4.value_is(v4.__ctobpl_const_11, inline$v4.Eval$0$op);
+ goto inline$v4.Eval$0$label_12#2;
+
+ inline$v4.Eval$0$label_12#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 41} true;
+ assert true;
+ v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR[v4.result__EXPR(inline$v4.Eval$0$e) := inline$v4.Eval$0$res];
+ assume v4.value_is(v4.__ctobpl_const_12, inline$v4.Eval$0$e);
+ assume v4.value_is(v4.__ctobpl_const_13, v4.Mem_T.result__EXPR[v4.result__EXPR(inline$v4.Eval$0$e)]);
+ assume v4.value_is(v4.__ctobpl_const_14, inline$v4.Eval$0$res);
+ goto inline$v4.Eval$0$label_1#2;
+
+ inline$v4.Eval$0$label_1#2:
+ assert {:sourcefile "c:\tvm\projects\symb_diff\symdiff\test\c_examples\ex3\v4\foo.c"} {:sourceline 42} true;
+ goto inline$v4.Eval$0$Return;
+
+ inline$v4.Eval$0$Return:
+ goto AA_INSTR_EQ_BODY$2;
+
+ AA_INSTR_EQ_BODY$2:
+ Output_of_v2.Eval_v4.Mem_T.result__EXPR := AA_TEMP10;
+ Output_of_v4.Eval_v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR;
+ AA_TEMP30 := AA_TEMP10 == v4.Mem_T.result__EXPR || (forall _x0: int :: AA_TEMP10[_x0] == v4.Mem_T.result__EXPR[_x0]);
+ return;
+}
+
+
+
+var Output_of_v2.EvalEntry1_v4.Mem_T.result__EXPR: [int]int;
+
+var Output_of_v4.EvalEntry1_v4.Mem_T.result__EXPR: [int]int;
+
+var Output_of_v2.EvalEntry1_v4.Mem_T.INT4: [int]int;
+
+var Output_of_v4.EvalEntry1_v4.Mem_T.INT4: [int]int;
+
+var Output_of_v2.EvalEntry1_v4.isUnsigned: int;
+
+var Output_of_v4.EvalEntry1_v4.isUnsigned: int;
+
+procedure EQ_v2.EvalEntry1__v4.EvalEntry1(e_.1: int, outval_.1: int) returns (AA_TEMP80: bool, AA_TEMP81: bool, AA_TEMP82: bool);
+ modifies v4.Mem_T.result__EXPR, v4.Mem_T.INT4, v4.isUnsigned, Output_of_v2.EvalEntry1_v4.Mem_T.result__EXPR, Output_of_v4.EvalEntry1_v4.Mem_T.result__EXPR, Output_of_v2.EvalEntry1_v4.Mem_T.INT4, Output_of_v4.EvalEntry1_v4.Mem_T.INT4, Output_of_v2.EvalEntry1_v4.isUnsigned, Output_of_v4.EvalEntry1_v4.isUnsigned;
+ ensures AA_TEMP82 && AA_TEMP81 && AA_TEMP80;
+
+
+
+implementation EQ_v2.EvalEntry1__v4.EvalEntry1(e_.1: int, outval_.1: int) returns (AA_TEMP80: bool, AA_TEMP81: bool, AA_TEMP82: bool)
+{
+ var AA_TEMP60: [int]int;
+ var AA_TEMP61: [int]int;
+ var AA_TEMP62: int;
+ var AA_TEMP50: [int]int;
+ var AA_TEMP51: [int]int;
+ var AA_TEMP52: int;
+
+ AA_INSTR_EQ_BODY:
+ AA_TEMP50 := v4.Mem_T.result__EXPR;
+ AA_TEMP51 := v4.Mem_T.INT4;
+ AA_TEMP52 := v4.isUnsigned;
+ call v2.EvalEntry1(e_.1, outval_.1);
+ AA_TEMP60 := v4.Mem_T.result__EXPR;
+ AA_TEMP61 := v4.Mem_T.INT4;
+ AA_TEMP62 := v4.isUnsigned;
+ v4.Mem_T.result__EXPR := AA_TEMP50;
+ v4.Mem_T.INT4 := AA_TEMP51;
+ v4.isUnsigned := AA_TEMP52;
+ call v4.EvalEntry1(e_.1, outval_.1);
+ Output_of_v2.EvalEntry1_v4.Mem_T.result__EXPR := AA_TEMP60;
+ Output_of_v4.EvalEntry1_v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR;
+ Output_of_v2.EvalEntry1_v4.Mem_T.INT4 := AA_TEMP61;
+ Output_of_v4.EvalEntry1_v4.Mem_T.INT4 := v4.Mem_T.INT4;
+ Output_of_v2.EvalEntry1_v4.isUnsigned := AA_TEMP62;
+ Output_of_v4.EvalEntry1_v4.isUnsigned := v4.isUnsigned;
+ AA_TEMP80, AA_TEMP81, AA_TEMP82 := AA_TEMP60 == v4.Mem_T.result__EXPR || (forall _x0: int :: AA_TEMP60[_x0] == v4.Mem_T.result__EXPR[_x0]), AA_TEMP61 == v4.Mem_T.INT4 || (forall _x0: int :: AA_TEMP61[_x0] == v4.Mem_T.INT4[_x0]), AA_TEMP62 == v4.isUnsigned;
+ return;
+}
+
+
+
+var Output_of_v2.EvalEntry2_v4.Mem_T.result__EXPR: [int]int;
+
+var Output_of_v4.EvalEntry2_v4.Mem_T.result__EXPR: [int]int;
+
+var Output_of_v2.EvalEntry2_v4.isUnsigned: int;
+
+var Output_of_v4.EvalEntry2_v4.isUnsigned: int;
+
+procedure EQ_v2.EvalEntry2__v4.EvalEntry2(e_.1: int) returns (AA_TEMP130: bool, AA_TEMP131: bool);
+ modifies v4.Mem_T.result__EXPR, v4.isUnsigned, Output_of_v2.EvalEntry2_v4.Mem_T.result__EXPR, Output_of_v4.EvalEntry2_v4.Mem_T.result__EXPR, Output_of_v2.EvalEntry2_v4.isUnsigned, Output_of_v4.EvalEntry2_v4.isUnsigned;
+ ensures AA_TEMP131 && AA_TEMP130;
+
+
+
+implementation EQ_v2.EvalEntry2__v4.EvalEntry2(e_.1: int) returns (AA_TEMP130: bool, AA_TEMP131: bool)
+{
+ var AA_TEMP110: [int]int;
+ var AA_TEMP111: int;
+ var AA_TEMP100: [int]int;
+ var AA_TEMP101: int;
+
+ AA_INSTR_EQ_BODY:
+ AA_TEMP100 := v4.Mem_T.result__EXPR;
+ AA_TEMP101 := v4.isUnsigned;
+ call v2.EvalEntry2(e_.1);
+ AA_TEMP110 := v4.Mem_T.result__EXPR;
+ AA_TEMP111 := v4.isUnsigned;
+ v4.Mem_T.result__EXPR := AA_TEMP100;
+ v4.isUnsigned := AA_TEMP101;
+ call v4.EvalEntry2(e_.1);
+ Output_of_v2.EvalEntry2_v4.Mem_T.result__EXPR := AA_TEMP110;
+ Output_of_v4.EvalEntry2_v4.Mem_T.result__EXPR := v4.Mem_T.result__EXPR;
+ Output_of_v2.EvalEntry2_v4.isUnsigned := AA_TEMP111;
+ Output_of_v4.EvalEntry2_v4.isUnsigned := v4.isUnsigned;
+ AA_TEMP130, AA_TEMP131 := AA_TEMP110 == v4.Mem_T.result__EXPR || (forall _x0: int :: AA_TEMP110[_x0] == v4.Mem_T.result__EXPR[_x0]), AA_TEMP111 == v4.isUnsigned;
+ return;
+}
+
+
+
+function _uf_v4.__HAVOC_malloc_new(arg_0: int) : int;
+
+function _uf_v2.__HAVOC_malloc_new(arg_0: int) : int;
+
+function _uf_v4.__HAVOC_det_malloc_new(arg_0: int) : int;
+
+function _uf_v2.__HAVOC_det_malloc_new(arg_0: int) : int;
+
+function _uf_v4.__HAVOC_memset_split_1_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int;
+
+function _uf_v2.__HAVOC_memset_split_1_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int;
+
+function _uf_v4.__HAVOC_memset_split_2_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int;
+
+function _uf_v2.__HAVOC_memset_split_2_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int;
+
+function _uf_v4.__HAVOC_memset_split_4_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int;
+
+function _uf_v2.__HAVOC_memset_split_4_ret(arg_0: [int]int, arg_1: int, arg_2: int, arg_3: int) : [int]int;
+
+function _uf_v4.nondet_choice_x() : int;
+
+function _uf_v2.nondet_choice_x() : int;
+
+function _uf_v4.det_choice_x() : int;
+
+function _uf_v2.det_choice_x() : int;
+
+function _uf_v4._strdup_new(arg_0: int) : int;
+
+function _uf_v2._strdup_new(arg_0: int) : int;
+
+function _uf_v4._xstrcasecmp_ret(arg_0: int, arg_1: int) : int;
+
+function _uf_v2._xstrcasecmp_ret(arg_0: int, arg_1: int) : int;
+
+function _uf_v4._xstrcmp_ret(arg_0: int, arg_1: int) : int;
+
+function _uf_v2._xstrcmp_ret(arg_0: int, arg_1: int) : int;
+
+function _uf_v4.Eval_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : [int]int;
+
+function _uf_v2.Eval_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : [int]int;
+
+function _uf_v4.EvalEntry1_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : [int]int;
+
+function _uf_v4.EvalEntry1_v4.Mem_T.INT4(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : [int]int;
+
+function _uf_v4.EvalEntry1_v4.isUnsigned(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : int;
+
+function _uf_v2.EvalEntry1_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : [int]int;
+
+function _uf_v2.EvalEntry1_v4.Mem_T.INT4(arg_0: int, arg_1: int, arg_2: int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: [int]int, arg_7: [int]int, arg_8: int) : [int]int;
+
+function _uf_v4.EvalEntry2_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : [int]int;
+
+function _uf_v4.EvalEntry2_v4.isUnsigned(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : int;
+
+function _uf_v2.EvalEntry2_v4.Mem_T.result__EXPR(arg_0: int, arg_1: int, arg_2: [int]int, arg_3: [int]int, arg_4: [int]int, arg_5: [int]int, arg_6: int) : [int]int;
diff --git a/Test/prover/runtest.bat b/Test/prover/runtest.bat
new file mode 100644
index 00000000..b9b64190
--- /dev/null
+++ b/Test/prover/runtest.bat
@@ -0,0 +1,13 @@
+@echo off
+setlocal
+
+set BGEXE=..\..\Binaries\Boogie.exe
+rem set BGEXE=mono ..\..\Binaries\Boogie.exe
+
+echo ==================== -z3multipleErrors ========================
+for %%f in (z3mutl.bpl EQ_v2.Eval__v4.Eval_out.bpl) do (
+ echo.
+ echo -------------------- %%f --------------------
+ %BGEXE% -typeEncoding:m -z3multipleErrors %* %%f
+)
+
diff --git a/Test/prover/z3mutl.bpl b/Test/prover/z3mutl.bpl
new file mode 100644
index 00000000..73cd62b1
--- /dev/null
+++ b/Test/prover/z3mutl.bpl
@@ -0,0 +1,22 @@
+var x:int;
+
+procedure Foo(){
+
+start:
+
+ goto L1, L2, L3, L4;
+L1: assume x == 1;
+ goto L5;
+
+L2: assume x == 2;
+ goto L5;
+
+L3: assume x == 3;
+ goto L5;
+
+L4: assume x > 10;
+ goto L5;
+
+L5: assert (x > 4);
+
+} \ No newline at end of file
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-07 02:50:25 +0000