diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-22 16:09:47 -0600 |
|---|---|---|
| committer | Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com> | 2020-01-22 14:09:47 -0800 |
| commit | 91538b206fd5da5be289cf2d6165a854e6e5bc07 (patch) | |
| tree | 698b7350997439c3d9f1c55d5728963329302cd5 | |
| parent | ac0bbd54de6e2b95514400c8f502aea95e5346c4 (diff) | |
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>
| -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); } |