diff options
Diffstat (limited to 'src')
| -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; |