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 4660005aacf0d8cfe0fd338e343baec0e5bdb6f1..2843e6fd28972794ca55e8415279cda484b5d2a0 100644 (file)
--- 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 (file)
index 0000000..4564287
--- /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 (file)
index 0000000..a065824
--- /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)