Goose  Artifact [c2c45f5df1]

Artifact c2c45f5df13ca29b4fa168b30fa700c8a3202649d4b5af80714b583ec2875b85:

• File tests/noprelude/verify/z3out-test-4.txt — part of check-in [353fcc252a] at 2020-01-04 15:17:12 on branch trunk —
  • verifier: check compilation-time function calls.
  • verifier: improved error messages wording.
  (user: achavasse size: 1185)

=== Checking compilation-time call ===

=== Checking compilation-time call ===

=== Checking compilation-time call ===

=== Checking compilation-time call ===

=== Checking compilation-time call ===

=== Begin function verification trace ===
assume (distinct v38 v39)
(= b1 true)
assume (= v40 v38)
assume (= v41 v39)
assume (= v42 v40)
assume (= v43 v41)
(= e1_2 (and b1 (< v42 v43)))
(= b2 e1_2)
(=> e1_2 (= v44 v43))
assume (=> b2 (= v45 v44))
(=> e1_2 (= v46 v42))
assume (=> b2 (= v47 v46))
assume (=> b2 (= v48 v45))
assume (=> b2 (= v49 v47))
(= e1_3 (and b1 (not (< v42 v43))))
(= e2_3 (and b2 b2))
(= b3 (or e1_3 e2_3))
(=> e1_3 (= v50 v42))
(=> e2_3 (= v50 v48))
(=> e1_3 (= v51 v43))
(=> e2_3 (= v51 v49))
check_unsat (and b3 (not (> (- v50 v51) 0)))
=== End function verification trace ===

=== Begin function verification trace ===
assume (distinct v52 0)
(= b1 true)
check_unsat (not (distinct v52 (* 2 v52)))
assume (> r53 0)
check_unsat (not (distinct r53 0))
=== End function verification trace ===

=== Checking compilation-time call ===
check_unsat (not (distinct 5 0))

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