From: Gereon Kremer <gkremer@cs.stanford.edu>
Date: Wed, 23 Feb 2022 23:06:31 +0000 (+0100)
Subject: Add two regressions related to RAN models (#8142)
X-Git-Tag: cvc5-1.0.0~391
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5c902c8c0bc8e7d8aaa543b048345495c7ec48cd;p=cvc5.git

Add two regressions related to RAN models (#8142)

This PR adds regressions for two issues that relate to the previously incomplete handling of real algebraic models.
The issue has been resolved by properly integrating real algebraic numbers as model values and in the rewriter.
Fixes #6547. Fixes #6619.
---

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4660005aa..2843e6fd2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -765,6 +765,8 @@ set(regress_0_tests
   regress0/nl/issue5737-div00.smt2
   regress0/nl/issue5740-mod00.smt2
   regress0/nl/issue5740-2-mod00.smt2
+  regress0/nl/issue6547-ran-model.smt2
+  regress0/nl/issue6619-ran-model.smt2
   regress0/nl/issue8135-icp-candidates.smt2
   regress0/nl/magnitude-wrong-1020-m.smt2
   regress0/nl/mult-po.smt2
diff --git a/test/regress/regress0/nl/issue6547-ran-model.smt2 b/test/regress/regress0/nl/issue6547-ran-model.smt2
new file mode 100644
index 000000000..45642873a
--- /dev/null
+++ b/test/regress/regress0/nl/issue6547-ran-model.smt2
@@ -0,0 +1,6 @@
+; REQUIRES: poly
+; EXPECT: sat
+(set-logic QF_NRA)
+(declare-const r Real)
+(assert (= 1.0 (/ 2 r r)))
+(check-sat)
diff --git a/test/regress/regress0/nl/issue6619-ran-model.smt2 b/test/regress/regress0/nl/issue6619-ran-model.smt2
new file mode 100644
index 000000000..a065824b0
--- /dev/null
+++ b/test/regress/regress0/nl/issue6619-ran-model.smt2
@@ -0,0 +1,8 @@
+; REQUIRES: poly
+; EXPECT: sat
+(set-logic QF_NRA)
+(declare-fun v () Bool)
+(declare-fun r () Real)
+(assert (> 1.0 (* r (- 1.0) (- 0.0 r 86.1))))
+(assert (or v (= 1.0 (/ 1.0 (- r 86.1)))))
+(check-sat)