From 387764620aa438a34bd78c2f18a6095350002c18 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 1 Mar 2022 20:38:21 -0600 Subject: [PATCH] Add regressions for fixed issues (#8202) Fixes #4463. Fixes cvc5/cvc5-projects#403. --- test/regress/CMakeLists.txt | 2 ++ test/regress/regress0/nl/issue4463-ack-model.smt2 | 6 ++++++ test/regress/regress0/nl/nta/proj-issue403.smt2 | 8 ++++++++ 3 files changed, 16 insertions(+) create mode 100644 test/regress/regress0/nl/issue4463-ack-model.smt2 create mode 100644 test/regress/regress0/nl/nta/proj-issue403.smt2 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) -- 2.30.2