diff options
| author | Aina Niemetz <aina.niemetz@gmail.com> | 2018-02-22 11:11:39 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-02-22 11:11:39 -0800 |
| commit | 54321626c1939b055b2b48f15e9bdb3844abb89c (patch) | |
| tree | b215e3aa9c9603c12ae7da9f27525e1088529faa /src/theory/theory_engine.cpp | |
| parent | 3c4702e9381998b72622607e25c1532cb1c55418 (diff) | |
Fixed disabling the BV equality slicer for quantifiers. (#1623)
This fixes an incorrect condition introduced in #1619 to disable the BV equality slicer.
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 8c5203e25..0c2857b11 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1929,7 +1929,7 @@ void TheoryEngine::staticInitializeBVOptions( bool useSlicer = true; if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_ON) { - if (!d_logicInfo.isPure(theory::THEORY_BV) && !d_logicInfo.isQuantified()) + if (!d_logicInfo.isPure(theory::THEORY_BV) || d_logicInfo.isQuantified()) throw ModalException( "Slicer currently only supports pure QF_BV formulas. Use " "--bv-eq-slicer=off"); @@ -1948,7 +1948,7 @@ void TheoryEngine::staticInitializeBVOptions( } else if (options::bitvectorEqualitySlicer() == bv::BITVECTOR_SLICER_AUTO) { - if ((!d_logicInfo.isPure(theory::THEORY_BV) && !d_logicInfo.isQuantified()) + if ((!d_logicInfo.isPure(theory::THEORY_BV) || d_logicInfo.isQuantified()) || options::incrementalSolving() || options::produceModels()) return; |