From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Tue, 11 Sep 2018 03:20:42 +0000 (-0500)
Subject: fix (#2446)
X-Git-Tag: cvc5-1.0.0~4663
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=945da3af1ea94aeabcd8f39b23a8741c6e41c358;p=cvc5.git

fix (#2446)
---

diff --git a/src/theory/quantifiers/sygus/sygus_repair_const.cpp b/src/theory/quantifiers/sygus/sygus_repair_const.cpp
index 89f04ffb6..fe1dc30a4 100644
--- 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;