Goose  Artifact [9f5d9e0a03]

Artifact 9f5d9e0a035c9f8fa46793b4d0375afd37a165cc1a06d4c023fe9f18b54a9eba:

• File tests/g0/verification/z3gen/e-z3gen-test-logic-or.txt — part of check-in [45f663093d] at 2021-09-12 13:42:15 on branch trunk — Adopted a new convention for source extensions: .g0 for prelude code (where most language features won't be available), .g1 for user code (user: achavasse size: 671)

=== Checking compilation-time expression ===

=== Begin function verification trace ===
(= b1 true)
assume (= v47 u46)
assume (= v48 false)
assume (= v50 u49)
assume (= v51 true)
(= e1_2 (and b1 (not v48)))
(= b2 e1_2)
(=> e1_2 (= v52 v51))
assume (=> b2 (= v53 v52))
assume (=> b2 (= v54 v53))
(= e1_3 (and b1 v48))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v55 true))
(=> e2_3 (= v56 v54))
assume (=> b3 (= v57 v56))
(=> e2_3 (= v55 v57))
assume (=> b3 (= v58 v55))
assume (=> b3 (= v60 u59))
assume (=> b3 (= v61 v58))
=== End function verification trace ===

=== Begin function verification trace ===
(= b1 true)
=== End function verification trace ===