Goose  Artifact [b32f4d247d]

Artifact b32f4d247d2c4dd3898d328c88ebfe8dcc736d579a2fb891c30f48b7392767f6:

• File tests/g0/verification/z3gen/e-z3gen-test-1.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: 677)

=== Begin function verification trace ===
(=> b1 (= v0_1_41 p0))
(=> b1 (= v1_1_43 u42))
(=> b1 (= v1_1_44 v0_1_41))
(= e1_2 (and b1 (distinct v1_1_44 5)))
(= b2 e1_2)
(=> b2 (= v1_2_45 5))
(= e1_3 (and b1 (not (distinct v1_1_44 5))))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(= e3_4 (and b3 b3))
(= b4 e3_4)
(=> e1_3 (= v1_3_46 v1_1_44))
(=> e2_3 (= v1_3_46 v1_2_45))
(=> b3 (= v1_3_47 v1_3_46))
(=> e3_4 (= v1_4_48 v1_3_47))
(=> b4 (= v1_4_49 v1_4_48))
check_unsat (and b4 (not (= v1_4_49 5)))
(= e4_5 (and b4 b4))
(= b5 e4_5)
=== End function verification trace ===

=== Begin function verification trace ===
(=> b1 (= v0_1_51 1))
=== End function verification trace ===