From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 22 Jan 2020 22:09:47 +0000 (-0600)
Subject: Fix substitution in nl solver (#3638)
X-Git-Tag: cvc5-1.0.0~3723
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=91538b206fd5da5be289cf2d6165a854e6e5bc07;p=cvc5.git

Fix substitution in nl solver (#3638)

* Fix for 3614

* Add regression

* Remove regression

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 3274867bb..eff810522 100644
--- a/src/theory/arith/nl_model.cpp
+++ b/src/theory/arith/nl_model.cpp
@@ -905,8 +905,7 @@ bool NlModel::simpleCheckModelLit(Node lit)
   if (!qvars.empty())
   {
     Assert(qvars.size() == qsubs.size());
-    Node slit =
-        lit.substitute(qvars.begin(), qvars.end(), qsubs.begin(), qsubs.end());
+    Node slit = arithSubstitute(lit, qvars, qsubs);
     slit = Rewriter::rewrite(slit);
     return simpleCheckModelLit(slit);
   }