summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/sygus/sygus_repair_const.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_repair_const.cpp')
-rw-r--r--src/theory/quantifiers/sygus/sygus_repair_const.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index bcd826799..b7611784d 100644
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -444,7 +444,7 @@ Node SygusRepairConst::getFoQuery(Node body,
Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
Trace("sygus-repair-const") << " Unfold the specification..." << std::endl;
- body = d_tds->evaluateWithUnfolding(body);
+ body = d_tds->rewriteNode(body);
Trace("sygus-repair-const-debug") << " ...got : " << body << std::endl;
Trace("sygus-repair-const") << " Introduce first-order vars..." << std::endl;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback