1 files changed, 2257 insertions, 2257 deletions
diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
index 80b50686..bd823c3f 100644
--- a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
+++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
@@ -1,2257 +1,2257 @@
-// RUN: %boogie -typeEncoding:m -z3multipleErrors "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-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 div 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 div 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;
+// RUN: %boogie -typeEncoding:m -z3multipleErrors "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+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 div 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 div 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;