From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 7 Feb 2020 01:12:29 +0000 (-0600)
Subject: Fix exact sqrt (#3721)
X-Git-Tag: cvc5-1.0.0~3677
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c98585d9913878cfe5328fe98fb4357f911b29b0;p=cvc5.git

Fix exact sqrt (#3721)

Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>
---

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)