diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/cegis.cpp')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp index 8d1bfd9b6..708bffe80 100644 --- a/src/theory/quantifiers/sygus/cegis.cpp +++ b/src/theory/quantifiers/sygus/cegis.cpp @@ -345,7 +345,7 @@ void Cegis::addRefinementLemma(Node lem) d_rl_vals.end()); } // rewrite with extended rewriter - slem = extendedRewrite(slem); + slem = d_tds->rewriteNode(slem); // collect all variables in slem expr::getSymbols(slem, d_refinement_lemma_vars); std::vector<Node> waiting; @@ -509,7 +509,7 @@ bool Cegis::getRefinementEvalLemmas(const std::vector<Node>& vs, Node lemcs = lem.substitute(vs.begin(), vs.end(), ms.begin(), ms.end()); Trace("sygus-cref-eval2") << "...under substitution it is : " << lemcs << std::endl; - Node lemcsu = vsit.doEvaluateWithUnfolding(d_tds, lemcs); + Node lemcsu = d_tds->rewriteNode(lemcs); Trace("sygus-cref-eval2") << "...after unfolding is : " << lemcsu << std::endl; if (lemcsu.isConst() && !lemcsu.getConst<bool>()) |