diff options
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/sygus/cegis.cpp | 8 |
1 files changed, 0 insertions, 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<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 |