From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Mon, 7 Dec 2020 13:25:08 +0000 (+0100)
Subject: Add regression from #4927 (#5556)
X-Git-Tag: cvc5-1.0.0~2494
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cbf6e1238ad355e7369f110385342c0a5ebb89d9;p=cvc5.git

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 a401836f5..09ce71577 100644
--- 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
index 000000000..ad967b48f
--- /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)