From 5c902c8c0bc8e7d8aaa543b048345495c7ec48cd Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Thu, 24 Feb 2022 00:06:31 +0100 Subject: [PATCH] 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. --- test/regress/CMakeLists.txt | 2 ++ test/regress/regress0/nl/issue6547-ran-model.smt2 | 6 ++++++ test/regress/regress0/nl/issue6619-ran-model.smt2 | 8 ++++++++ 3 files changed, 16 insertions(+) create mode 100644 test/regress/regress0/nl/issue6547-ran-model.smt2 create mode 100644 test/regress/regress0/nl/issue6619-ran-model.smt2 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) -- 2.30.2