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 a495239dd1b5dea7cfc9600ab23590ab5e61bd5d..0439943680aa8c12c0b284bce9e2e0bcd3ea1c86 100644 (file)
--- 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 (file)
index 0000000..82256b7
--- /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 (file)
index 0000000..7f54681
--- /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)