diff options
author | yoni206 <yoni206@users.noreply.github.com> | 2018-07-26 15:16:04 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-07-26 15:16:04 -0700 |
commit | 68de263452bbde839f0bec7896e3f85a8ab8fb9e (patch) | |
tree | 791c107608801bbdcbcffa7413b3a86710f9fcf3 /src | |
parent | 21e1d582ecbb92f62f4a23a338b0455b2ebe5538 (diff) |
Disabling bvLazyRewriteExtf in the right place (#2214)
Diffstat (limited to 'src')
-rw-r--r-- | src/smt/smt_engine.cpp | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 42d8c4730..d807567b7 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1767,11 +1767,6 @@ void SmtEngine::setDefaults() { options::bvEagerExplanations.set(true); } - if( !options::bitvectorEqualitySolver() ){ - Trace("smt") << "disabling bvLazyRewriteExtf since equality solver is disabled" << endl; - options::bvLazyRewriteExtf.set(false); - } - // Turn on arith rewrite equalities only for pure arithmetic if(! options::arithRewriteEq.wasSetByUser()) { bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isQuantified(); @@ -2320,6 +2315,22 @@ void SmtEngine::setDefaults() { options::bitvectorInequalitySolver.set(false); } } + + if (!options::bitvectorEqualitySolver()) + { + if (options::bvLazyRewriteExtf()) + { + if (options::bvLazyRewriteExtf.wasSetByUser()) + { + throw OptionException( + "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set"); + } + } + Trace("smt") + << "disabling bvLazyRewriteExtf since equality solver is disabled" + << endl; + options::bvLazyRewriteExtf.set(false); + } } void SmtEngine::setProblemExtended(bool value) |