From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 26 Oct 2021 17:10:50 +0000 (-0500)
Subject: Add regressions for fixed issues (#7495)
X-Git-Tag: cvc5-1.0.0~967
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=58e710b299aaf46d480085fb98c77cd3b60de04a;p=cvc5.git

Add regressions for fixed issues (#7495)

Fixes #4656. Fixes #5234. These do not occur on master.
---

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8263152dd..299261284 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -449,6 +449,7 @@ set(regress_0_tests
   regress0/cores/issue4971-2.smt2
   regress0/cores/issue4971-3.smt2
   regress0/cores/issue5079.smt2
+  regress0/cores/issue5234-uc-ua.smt2 
   regress0/cores/issue5238.smt2
   regress0/cores/issue5902.smt2
   regress0/cores/issue5908.smt2
@@ -1453,6 +1454,7 @@ set(regress_0_tests
   regress0/unconstrained/geq.smt2
   regress0/unconstrained/gt.smt2
   regress0/unconstrained/issue4644.smt2
+  regress0/unconstrained/issue4656-bool-term-vars.smt2
   regress0/unconstrained/ite.smt2
   regress0/unconstrained/leq.smt2
   regress0/unconstrained/lt.smt2
diff --git a/test/regress/regress0/cores/issue5234-uc-ua.smt2 b/test/regress/regress0/cores/issue5234-uc-ua.smt2
new file mode 100644
index 000000000..ab31ec71f
--- /dev/null
+++ b/test/regress/regress0/cores/issue5234-uc-ua.smt2
@@ -0,0 +1,12 @@
+; EXPECT: unsat
+; EXPECT: ()
+(set-option :incremental true)
+(set-option :check-unsat-cores true)
+(set-option :produce-unsat-assumptions true)
+(set-logic ALL)
+(declare-const a Bool)
+(declare-const b Bool)
+(declare-const c Bool)
+(assert (distinct a b c))
+(check-sat-assuming (c))
+(get-unsat-assumptions)
diff --git a/test/regress/regress0/unconstrained/issue4656-bool-term-vars.smt2 b/test/regress/regress0/unconstrained/issue4656-bool-term-vars.smt2
new file mode 100644
index 000000000..cd6154464
--- /dev/null
+++ b/test/regress/regress0/unconstrained/issue4656-bool-term-vars.smt2
@@ -0,0 +1,12 @@
+(set-logic QF_AUFBVLIA)
+(set-info :status unsat)
+(declare-fun a (Bool) Bool)
+(declare-fun b (Bool) Bool)
+(declare-fun c (Bool) Bool)
+(declare-fun d () Bool)
+(declare-fun e () Bool)
+(declare-fun f () Bool)
+(assert (distinct (a d) (a e)))
+(assert (distinct (b e) (b f)))
+(assert (distinct (c f) (c d)))
+(check-sat)