diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-02-06 19:12:29 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-02-06 17:12:29 -0800 |
commit | c98585d9913878cfe5328fe98fb4357f911b29b0 (patch) | |
tree | dfa4b4e2b29f69489243778b8beb57e5581c4ecd /test/regress | |
parent | babbe0e30d769b5f68cb3f36820fbb5e176de7c5 (diff) |
Fix exact sqrt (#3721)
Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
Diffstat (limited to 'test/regress')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/nl/issue3719.smt2 | 5 |
2 files changed, 6 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 35d604768..ef33adb59 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -558,6 +558,7 @@ set(regress_0_tests regress0/nl/issue3411.smt2 regress0/nl/issue3475.smt2 regress0/nl/issue3652.smt2 + regress0/nl/issue3719.smt2 regress0/nl/magnitude-wrong-1020-m.smt2 regress0/nl/mult-po.smt2 regress0/nl/nia-wrong-tl.smt2 diff --git a/test/regress/regress0/nl/issue3719.smt2 b/test/regress/regress0/nl/issue3719.smt2 new file mode 100644 index 000000000..c620432f4 --- /dev/null +++ b/test/regress/regress0/nl/issue3719.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_NRA) +(set-info :status sat) +(declare-fun a () Real) +(assert (= (* 4 a a) 9)) +(check-sat) |