From 5418990bd91dc0bdae24c10ddd1bc7ccf1c2dce2 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 30 Apr 2018 13:13:22 -0500 Subject: [PATCH] Fix 1156 (#1830) --- src/theory/quantifiers/sygus/cegis.cpp | 8 -------- 1 file changed, 8 deletions(-) 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& 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 -- 2.30.2