From 91538b206fd5da5be289cf2d6165a854e6e5bc07 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 22 Jan 2020 16:09:47 -0600 Subject: [PATCH] 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> --- src/theory/arith/nl_model.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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); } -- 2.30.2