Goose  Artifact [b8c5a104ed]

Artifact b8c5a104ed90e9afffd80d8c86c6d36ad42c9f3d4c26a1314f9899f2e19f836b:

• File tests/noprelude/verify/z3out-test-2.txt — part of check-in [077c944c02] at 2020-06-05 00:35:45 on branch trunk — Verifier: handle "StoreToAddress" for addresses that point to tuple members. (user: achavasse size: 611) [more...]

=== Checking compilation-time call ===

=== Checking compilation-time call ===

=== Begin function verification trace ===
assume (distinct p0 p1)
(= b1 true)
(= e1_2 (and b1 (< p0 p1)))
(= b2 e1_2)
(=> e1_2 (= v34 p1))
(=> e1_2 (= v36 p0))
(= e1_3 (and b1 (not (< p0 p1))))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v37 p0))
(=> e2_3 (= v37 v34))
(=> e1_3 (= v38 p1))
(=> e2_3 (= v38 v36))
check_unsat (and b3 (not (> v37 v38)))
=== End function verification trace ===

=== Begin function verification trace ===
(= b1 true)
check_unsat (not (distinct 2 1))
=== End function verification trace ===