(define a::int)
(define b::int)
(define c::int)
(define d::int)

(push)
(assert (= (+ a b c) 0))
(echo "\nAFTER (push) (assert (= (+ a b c) 0))\n")
(dump-context)
(echo "===============================\n")

(push)
(assert (> (+ a d) 0))
(echo "\nAFTER (push) (assert (> (+ a d) 0))\n")
(dump-context)
(echo "===============================\n")

(push)
(assert (and (= b 1) (= c 1)))
(echo "\nAFTER (push) (assert (and (= b 1) (= c 1)))\n")
(dump-context)
(echo "===============================\n")

(push)
(assert (> a 1))
(echo "\nAFTER (push) (assert (> a 1))\n")
(dump-context)
(echo "===============================\n")

(push)
(echo "\nFIRST CHECK: unsat expected\n")
(check) 
(show-model)

(echo "\nAFTER (push)(check)\n") 
(dump-context)
(echo "===============================\n")

(pop)
(echo "\nAFTER (pop)\n")
(dump-context)
(echo "===============================\n")

(echo "\nSECOND CHECK: unsat expected\n");
(check)

(echo "\nAFTER (check)\n")
(dump-context)
(echo "===============================\n")

(pop)
(echo "\nAFTER (pop)\n")
(dump-context)
(echo "===============================\n")

(echo "\nTHIRD CHECK: sat expected\n")
(check)
(show-model)

(echo "\nAFTER (check)\n")
(dump-context)
(echo "===============================\n")

(pop)
(echo "\nAFTER (pop)\n")
(dump-context)
(echo "===============================\n")

(echo "\nFOURTH CHECK: sat expected\n")
(check)
(show-model)

(echo "\nAFTER (check)\n")
(dump-context)
(echo "===============================\n")

(pop)
(echo "\nAFTER (pop)\n")
(dump-context)
(echo "===============================\n")


(echo "\nFIFTH CHECK: sat expected\n")
(check)
(show-model)

(echo "\nAFTER (check)\n")
(dump-context)
(echo "===============================\n")

(pop)
(echo "\nAFTER (pop)\n")
(dump-context)
(echo "===============================\n")

(echo "\nSIXTH CHECK: sat expected\n")
(check)
(show-model)

(echo "\nAFTER (check)\n")
(dump-context)
(echo "===============================\n")

(pop) ;; should report an error

(echo "\nAFTER FAILED (pop)\n")
(dump-context)
(echo "===============================\n")