path: root/test/regress/regress1/quantifiers/issue4433-nqe.smt2

(set-logic LIA)
(set-option :cegqi-nested-qe true)
(set-info :status unsat)
(assert
 (forall ((a Int) (b Int))
 (xor (xor (= a 0) (= b 0))
  (forall ((c Int))
  (= (ite (= a 0) 0 1) (ite (= c 0) 0 1))))))
(check-sat)