Fixed disabling the BV equality slicer for quantifiers. (#1623)

This fixes an incorrect condition introduced in #1619 to disable the BV equality slicer.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 8c5203e256b6e3e891876333235e2042c5dc11a3..0c2857b11a268e8e30ce4eda2b3966c0496c2d8d 100644 (file)
--- 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;