Regression

ajreynol · Feb 24, 2025 · a225d21 · a225d21
1 parent b9860a7
commit a225d21
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 0 deletions.
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
@@ -1572,6 +1572,7 @@ set(regress_0_tests
   regress0/quantifiers/proj-issue152-2-non-std-nterm-ext-rew.smt2
   regress0/quantifiers/proj-issue512-has-skolem.smt2
   regress0/quantifiers/proj-issue608-mbqi-cegqi.smt2
+  regress0/quantifiers/proj-issue722-qpre.smt2
   regress0/quantifiers/proj-issue763-no-gt-purify-bool.smt2
   regress0/quantifiers/pure_dt_cbqi.smt2
   regress0/quantifiers/qarray-sel-over-store.smt2

diff --git a/test/regress/cli/regress0/quantifiers/proj-issue722-qpre.smt2 b/test/regress/cli/regress0/quantifiers/proj-issue722-qpre.smt2
@@ -0,0 +1,7 @@
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :prenex-quant norm)
+(declare-const x Bool)
+(assert (not (or x (forall ((_x (Array Int Bool))) (or (not x) (not (select _x 0)))))))
+(assert (exists ((_x (Array Int Bool))) (and (select _x 0))))
+(check-sat)