From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 30 Apr 2018 18:13:22 +0000 (-0500)
Subject: Fix 1156 (#1830)
X-Git-Tag: cvc5-1.0.0~5109
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5418990bd91dc0bdae24c10ddd1bc7ccf1c2dce2;p=cvc5.git

Fix 1156 (#1830)
---

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index b778b90be..ab448a2b8 100644
--- a/src/theory/quantifiers/sygus/cegis.cpp
+++ b/src/theory/quantifiers/sygus/cegis.cpp
@@ -16,8 +16,6 @@
 #include "options/quantifiers_options.h"
 #include "theory/quantifiers/sygus/ce_guided_conjecture.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
-// FIXME : remove these includes (github issue #1156)
-#include "theory/bv/theory_bv_rewriter.h"
 #include "theory/theory_engine.h"
 
 using namespace std;
@@ -128,12 +126,6 @@ bool Cegis::constructCandidates(const std::vector<Node>& enums,
       Node lem = nm->mkNode(kind::OR,
                             eager_exps[j].negate(),
                             eager_terms[j].eqNode(eager_vals[j]));
-      if (d_qe->getTheoryEngine()->isTheoryEnabled(THEORY_BV))
-      {
-        // FIXME: hack to incorporate hacks from BV for division by zero
-        // (github issue #1156)
-        lem = bv::TheoryBVRewriter::eliminateBVSDiv(lem);
-      }
       if (d_qe->addLemma(lem))
       {
         Trace("cegqi-lemma") << "Cegqi::Lemma : evaluation : " << lem