test2.smt2

(declare-fun a () Int)
(declare-fun b () Double)
(declare-fun c () Float)
(declare-fun d () Int)

(declare-fun E0 () Bool)
(declare-fun c0 () Bool)
(declare-fun f0 () Bool)
(declare-fun f1 () Bool)
(declare-fun z () Bool)
(declare-fun y () Bool)
(declare-fun x () Bool)

(push 1)
(assert (and a))
(assert (and b))
(assert (and c))
(assert (and d))
(assert (and a b c d))
(assert (let ((.def_11 (+ (- E0))) (.def_12 (/ f1))) (* .def_11 .def_12) ) ) 
(assert (let ((.def_10 (not f0))) (* .def_10 1)))
(assert (let ((.def_10 (not f0))) (+ .def_10 1)))
(assert (let ((.def_11 (+ (- E0))) (.def_12 (/ f1))) (* .def_11 .def_12) ) ) 
(assert (let ((.def_10 (not f0))) (/ .def_10 1)))
(assert (let ((.def_11 (not E0)) (.def_12 (not f1)) (.def_12 (not f1))) (+ .def_11 .def_12) ) ) 
(assert (and E0 c0 E0))
(assert (and E0 f0 E0))
(assert (and f0 c0 f0 c0))
(assert (+ E0 c0))
(assert (+ (+ E0 c0) (+ E0 c0) ))
(assert (+ (+ E0 c0) (* E0 c0) ))
(assert (+ (+ E0 c0) (/ E0 c0) ))
(assert (+ (- E0 c0) (+ E0 c0) ))
(assert (+ (- E0 c0) (- E0 c0) ))
(assert (+ (- E0 c0) (* E0 c0) ))
(assert (+ (- E0 c0) (/ E0 c0) ))
(assert (/ E0 f0))
(assert (/ f0 E0))
(assert (/ z y))
(assert (/ y y))
(assert (/ y (/ y y)))
(assert ( forall ((x Int)) (> (p x) 0) ))
(assert (+ f0 E0))
(assert (* E0 c0))
(assert (* f0 E0))
(assert (* E0 c0 f0))
(assert ( forall ((x Int)) (> (p x) 0) ))
(assert (/ E0 E0 E0))
(assert (/ f0 E0 f1))
(assert (* f0 E0 f1))
(assert ( forall ((x Int)) (> (p x) 0) ))
(assert (+ E0 c0 f0))
(assert (+ f0 E0 f1))
(assert (and a b a b))
(assert ( forall ((x Int)) (> (p x) 0) ))
(check-sat)
(pop 1)
(assert (xor f0 f1))
(push 1)
(assert (and (and c0 E0)))
(assert (and c0 E0 (and f1)))
(assert (and E0 c0 E0))
(assert (and E0 f1 E0))
(assert (and E0 f0 E0))
(check-sat)
(pop 1)
(check-sat)
(exit)