diff options
| -rw-r--r-- | src/theory/arith/nl_model.cpp | 3 |
1 files changed, 1 insertions, 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); } |