(set-logic QF_ABV)
(declare-fun v7 () Bool)
(declare-fun v19 () Bool)
(declare-fun v29 () Bool)
(declare-fun v57 () Bool)
(declare-fun v71 () Bool)
(define-fun |Scoreboardh#805| () Bool (and v19 (or v7 v29)))
(assert (and (= v19 (= v29 true)) (= (or v7 v29) v71)))
(assert v19)
;(push 1)
;(assert false)
(set-info :status sat)
(check-sat)
;(pop 1)
(set-info :status sat)
(assert (and v57 v71))
(check-sat)
(exit)