1 files changed, 19 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 b/test/regress/regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
new file mode 100644
index 000000000..4d5cf4ec4
--- /dev/null
+++ b/test/regress/regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --cbqi --decision=internal
+; EXPECT: unsat
+(set-logic LIA)
+(set-info :status unsat)
+
+(assert (or 
+(forall ((H Int) (G Int)) (= (= G 0) (= H 0)))
+
+(forall ((C Int) (D Int) (E Int)) (or 
+(= (= D 0) (= C 0)) 
+(and 
+(not (forall ((G Int)) (= (= E 0) (= G 0)))) 
+(not (forall ((A Int)) 
+  (not (= (ite (= A 0) 0 1) (ite (= C 0) 0 2)))
+))
+)))
+))
+
+(check-sat)