From c98585d9913878cfe5328fe98fb4357f911b29b0 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 6 Feb 2020 19:12:29 -0600 Subject: [PATCH] Fix exact sqrt (#3721) Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> --- src/theory/arith/nl_model.cpp | 4 ++-- test/regress/CMakeLists.txt | 1 + test/regress/regress0/nl/issue3719.smt2 | 5 +++++ 3 files changed, 8 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress0/nl/issue3719.smt2 diff --git a/src/theory/arith/nl_model.cpp b/src/theory/arith/nl_model.cpp index eff810522..54ae4c52a 100644 --- a/src/theory/arith/nl_model.cpp +++ b/src/theory/arith/nl_model.cpp @@ -1200,8 +1200,8 @@ bool NlModel::getApproximateSqrt(Node c, Node& l, Node& u, unsigned iter) const Rational curr_sq = curr * curr; if (curr_sq == rc) { - rl = curr_sq; - ru = curr_sq; + rl = curr; + ru = curr; break; } else if (curr_sq < rc) 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) -- 2.30.2