summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_unif_strat.cpp')
-rw-r--r--src/theory/quantifiers/sygus/sygus_unif_strat.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
index 10db1ef9e..6b023075b 100644
--- a/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
+++ b/src/theory/quantifiers/sygus/sygus_unif_strat.cpp
@@ -264,7 +264,7 @@ void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren);
Trace("sygus-unif-debug2") << " Test evaluation of " << eut << "..."
<< std::endl;
- eut = d_tds->getEvalUnfold()->unfold(eut);
+ eut = d_tds->rewriteNode(eut);
Trace("sygus-unif-debug2") << " ...got " << eut;
Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback