From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 2 Mar 2022 02:38:21 +0000 (-0600)
Subject: Add regressions for fixed issues (#8202)
X-Git-Tag: cvc5-1.0.0~349
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=387764620aa438a34bd78c2f18a6095350002c18;p=cvc5.git

Add regressions for fixed issues (#8202)

Fixes #4463.
Fixes cvc5/cvc5-projects#403.
---

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index a495239dd..043994368 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -771,6 +771,7 @@ set(regress_0_tests
   regress0/nl/issue3971.smt2
   regress0/nl/issue3991.smt2
   regress0/nl/issue4007-rint-uf.smt2
+  regress0/nl/issue4463-ack-model.smt2
   regress0/nl/issue5534-no-assertions.smt2
   regress0/nl/issue5726-downpolys.smt2
   regress0/nl/issue5726-sqfactor.smt2
@@ -799,6 +800,7 @@ set(regress_0_tests
   regress0/nl/nta/issue8182-exact-mv-keep.smt2
   regress0/nl/nta/issue8182-2-exact-mv-keep.smt2
   regress0/nl/nta/issue8183-tc-pi.smt2
+  regress0/nl/nta/proj-issue403.smt2
   regress0/nl/nta/proj-issue460-pi-value.smt2
   regress0/nl/nta/real-pi.smt2
   regress0/nl/nta/sin-sym.smt2
diff --git a/test/regress/regress0/nl/issue4463-ack-model.smt2 b/test/regress/regress0/nl/issue4463-ack-model.smt2
new file mode 100644
index 000000000..82256b75e
--- /dev/null
+++ b/test/regress/regress0/nl/issue4463-ack-model.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic QF_NIA)
+(set-option :ackermann true)
+(assert (= (mod 75 0) 683))
+(check-sat)
diff --git a/test/regress/regress0/nl/nta/proj-issue403.smt2 b/test/regress/regress0/nl/nta/proj-issue403.smt2
new file mode 100644
index 000000000..7f546818c
--- /dev/null
+++ b/test/regress/regress0/nl/nta/proj-issue403.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(set-info :status sat)
+(set-option :global-declarations true)
+(declare-const _x1 Real)
+(assert (let ((_let0 real.pi))(<= (/ _let0 _x1) _let0)))
+(check-sat)