(echo "\nBASE\n")
(dump-context)
(echo "===============================\n")
(push)

(define a::int)
(define b::int)
(define c::int)
(assert (= (+ a b c) 0))
(echo "AFTER (assert (= (+ a b c) 0))\n")
(dump-context)
(echo "===============================\n")

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

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

(define d::int)
(assert (> (+ a d) 0))
(echo "AFTER (assert (> (+ a d) 0))\n")
(dump-context)
(echo "===============================\n")


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

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

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

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

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

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

(echo "FOURTH CHECK: unsat expected\n")
(check)

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

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