Goose  Artifact [995b379865]

Artifact 995b379865d61483a465e3ff573517897346275ee4d5d2ac077183b6babf0c1f:

• File tests/g0/verification/z3gen/e-z3gen-test-2.txt — part of check-in [b4d5bdf6ec] at 2022-06-18 18:51:47 on branch cir-stack-language —
  • Added a location id to all CIR instructions (needed with the stack based approach to locate intermediate results)
  • Fixed a bunch of verifier errors
  • Re-enabled most verifier tests, other than some requiring to re-implement a few more bits
  (user: zlodo size: 1361)

=== Begin function verification trace ===
(=> b1 (= v0_1_41 p0))
(=> b1 (= v1_1_42 p1))
assume (distinct v0_1_41 v1_1_42)
(=> b1 (= v3_1_44 u43))
(=> b1 (= v3_1_45 v0_1_41))
(=> b1 (= v4_1_47 u46))
(=> b1 (= v4_1_48 v1_1_42))
(=> b1 (= v5_1_50 u49))
(=> b1 (= v5_1_51 v3_1_45))
(=> b1 (= v6_1_53 u52))
(=> b1 (= v6_1_54 v4_1_48))
(= e1_2 (and b1 (< v5_1_51 v6_1_54)))
(= b2 e1_2)
(=> b2 (= v8_2_56 u55))
(=> e1_2 (= v6_2_57 v6_1_54))
(=> b2 (= v6_2_58 v6_2_57))
(=> b2 (= v8_2_59 v6_2_58))
(=> b2 (= v9_2_61 u60))
(=> e1_2 (= v5_2_62 v5_1_51))
(=> b2 (= v5_2_63 v5_2_62))
(=> b2 (= v9_2_64 v5_2_63))
(=> b2 (= v5_2_65 v8_2_59))
(=> b2 (= v6_2_66 v9_2_64))
(= e1_3 (and b1 (not (< v5_1_51 v6_1_54))))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(= e3_4 (and b3 b3))
(= b4 e3_4)
(=> e1_3 (= v5_3_67 v5_1_51))
(=> e2_3 (= v5_3_67 v5_2_65))
(=> b3 (= v5_3_68 v5_3_67))
(=> e3_4 (= v5_4_69 v5_3_68))
(=> b4 (= v5_4_70 v5_4_69))
(=> e1_3 (= v6_3_71 v6_1_54))
(=> e2_3 (= v6_3_71 v6_2_66))
(=> b3 (= v6_3_72 v6_3_71))
(=> e3_4 (= v6_4_73 v6_3_72))
(=> b4 (= v6_4_74 v6_4_73))
check_unsat (and b4 (not (> v5_4_70 v6_4_74)))
(= e4_5 (and b4 b4))
(= b5 e4_5)
=== End function verification trace ===

=== Begin function verification trace ===
(=> b1 (= v1_1_76 1))
(=> b1 (= v0_1_77 2))
check_unsat (not (distinct v0_1_77 v1_1_76))
=== End function verification trace ===