projects / cvc5.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: 0d997c9)
fix (#2446)
authorHaniel Barbosa <hanielbbarbosa@gmail.com>
Tue, 11 Sep 2018 03:20:42 +0000 (22:20 -0500)
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 11 Sep 2018 03:20:42 +0000 (22:20 -0500)
src/theory/quantifiers/sygus/sygus_repair_const.cpp patch | blob | history

diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 89f04ffb69392b1a7ec9729f7b84113fe6bd9ee1..fe1dc30a41dd655f9845f18a7500dd2ba6d280cf 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_repair_const.cpp
+++ b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
@@ -255,7 +255,7 @@ bool SygusRepairConst::repairSolution(const std::vector<Node>& candidates,
 
   Trace("cegqi-engine") << "Repairing previous solution..." << std::endl;
   // make the satisfiability query
-  bool needExport = false;
+  bool needExport = true;
   ExprManagerMapCollection varMap;
   ExprManager em(nm->getOptions());
   std::unique_ptr<SmtEngine> repcChecker;