Fix 1156 (#1830)

diff --git a/src/theory/quantifiers/sygus/cegis.cpp b/src/theory/quantifiers/sygus/cegis.cpp
index b778b90be2300a87c05fc4f48f6a2b47c52ca9d1..ab448a2b877329519ae0061e0e0c8f79daaf6e20 100644 (file)
--- 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