(set-info :status unsat)
(set-option :produce-unsat-cores true)
(declare-const x Bool)
(declare-const x3 Bool)
(assert (ite x true x3))
(push 1)
(assert (= x3 x))
(assert x)
(push 1)
(assert (not x3))
(check-sat)