(set-option :produce-assertions true)
; (set-option :interactive-mode true)
(get-option :produce-assertions)
(set-logic QF_UF)
(declare-fun a () Bool)
(declare-fun b () Bool)
(assert (or (! a :named aa) (! b :named bb)))
(get-assertions)
(push)
  (assert (not (and a bb)))
  (get-assertions)
(pop)
(get-assertions)