Goose  Artifact [415ec5c779]

Artifact 415ec5c779439240312e0c971aa1a00c3885b41c5063b53a222382cb01db6628:

• File tests/noprelude/verify/z3out-test-4.txt — part of check-in [b414bc18df] at 2019-10-12 17:25:06 on branch trunk — Verifier: use z3 push/pop to check assertions one at a time, so that we can find and report multiple errors in the same function. (user: achavasse size: 1353)

(declare-fun v1 () Int)
(declare-fun v0 () Int)
(declare-fun b0 () Bool)
(declare-fun v2 () Int)
(declare-fun v3 () Int)
(declare-fun v4 () Int)
(declare-fun v5 () Int)
(declare-fun b0_1 () Bool)
(declare-fun b1 () Bool)
(declare-fun v7 () Int)
(declare-fun v6 () Int)
(declare-fun v9 () Int)
(declare-fun v8 () Int)
(declare-fun v10 () Int)
(declare-fun v11 () Int)
(declare-fun b0_2 () Bool)
(declare-fun b1_2 () Bool)
(declare-fun b2 () Bool)
(declare-fun v12 () Int)
(declare-fun v13 () Int)
(assert (distinct v0 v1))
(assert (= b0 true))
(assert (= v2 v0))
(assert (= v3 v1))
(assert (= v4 v2))
(assert (= v5 v3))
(assert (= b0_1 (and b0 (< v4 v5))))
(assert (= b1 b0_1))
(assert (=> b0_1 (= v7 v5)))
(assert (=> b1 (= v6 v7)))
(assert (=> b0_1 (= v9 v4)))
(assert (=> b1 (= v8 v9)))
(assert (=> b1 (= v10 v6)))
(assert (=> b1 (= v11 v8)))
(assert (= b0_2 (and b0 (not (< v4 v5)))))
(assert (= b1_2 b1))
(assert (= b2 (or b0_2 b1_2)))
(assert (=> b0_2 (= v12 v4)))
(assert (=> b1_2 (= v12 v10)))
(assert (=> b0_2 (= v13 v5)))
(assert (=> b1_2 (= v13 v11)))
check: (and b2 (not (> (- v12 v13) 0)))

(declare-fun v0 () Int)
(declare-fun b0 () Bool)
(declare-fun r1 () Int)
(assert (distinct v0 0))
(assert (= b0 true))
(assert (> r1 0))
check: (not (distinct v0 (* 2 v0)))
check: (not (distinct r1 0))

(declare-fun b0 () Bool)
(assert (= b0 true))