From 54321626c1939b055b2b48f15e9bdb3844abb89c Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Thu, 22 Feb 2018 11:11:39 -0800 Subject: [PATCH] Fixed disabling the BV equality slicer for quantifiers. (#1623) This fixes an incorrect condition introduced in #1619 to disable the BV equality slicer. --- src/theory/theory_engine.cpp | 4 ++-- 1 file 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; -- 2.30.2