diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-30 13:13:22 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-30 13:13:22 -0500 |
| commit | 5418990bd91dc0bdae24c10ddd1bc7ccf1c2dce2 (patch) | |
| tree | 38fd636ebb9defb7db2e1392e262f6de00bd40a0 | |
| parent | c938344a9a524dd51f4c80c360dd28cd06f228ac (diff) | |
Fix 1156 (#1830)
| -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 |