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 3274867bb7d6af72037140c0806f7e7f1aaaf478..eff810522c991dbc6c670f4e1389f1d8ad385a52 100644 (file)
--- 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);
   }