Add regression from #4927 (#5556)

The error from #4927 has been fixed in the meantime, this PR adds the example as regression.
Closes #4927.

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a401836f51f2eb4ca01df0e77be60feeb885b4b2..09ce71577528e60ae84fa1667e7d65a4f139ab3a 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -91,6 +91,7 @@ set(regress_0_tests
   regress0/arrays/incorrect9.smtv1.smt2
   regress0/arrays/issue3813-massign-assert.smt2
   regress0/arrays/issue3814.smt2
+  regress0/arrays/issue4927-unsat-cores.smt2
   regress0/arrays/swap_t1_np_nf_ai_00005_007.cvc.smtv1.smt2
   regress0/arrays/x2.smtv1.smt2
   regress0/arrays/x3.smtv1.smt2

diff --git a/test/regress/regress0/arrays/issue4927-unsat-cores.smt2 b/test/regress/regress0/arrays/issue4927-unsat-cores.smt2
new file mode 100644 (file)
index 0000000..ad967b4
--- /dev/null
+++ b/test/regress/regress0/arrays/issue4927-unsat-cores.smt2
@@ -0,0 +1,12 @@
+; COMMANDLINE: --check-unsat-cores --check-models
+; EXPECT: unsat
+(set-logic QF_AX)
+(declare-const a (Array Bool Bool))
+(declare-const b (Array Bool Bool))
+(declare-const c Bool)
+(declare-const d Bool)
+(declare-const e Bool)
+(assert (= a (store b c d)))
+(assert (distinct e d (ite e c d)))
+(assert (= e c (select b d)))
+(check-sat)