diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-08 16:51:54 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-05-08 16:52:20 -0400 |
commit | a2c0fd92782ce942a6f25f2561a4918fb2c5b020 (patch) | |
tree | c976291b6aa9cc76244bb761c3db68cf7856a217 /src/smt | |
parent | 3f8927c16764151ed217b509a60e22336a2981de (diff) |
final updates for smt-eval script
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 75cffefc2..0bfc6e634 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -848,11 +848,10 @@ void SmtEngine::setLogicInternal() throw() { Trace("smt") << "setting uf symmetry breaker to " << qf_uf << endl; options::ufSymmetryBreaker.set(qf_uf); } - // by default, nonclausal simplification is off for QF_SAT and for quantifiers + // by default, nonclausal simplification is off for QF_SAT if(! options::simplificationMode.wasSetByUser()) { bool qf_sat = d_logic.isPure(THEORY_BOOL) && !d_logic.isQuantified(); - bool quantifiers = d_logic.isQuantified(); - Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat && !quantifiers) << endl; + Trace("smt") << "setting simplification mode to <" << d_logic.getLogicString() << "> " << (!qf_sat) << endl; //simplification=none works better for SMT LIB benchmarks with quantifiers, not others //options::simplificationMode.set(qf_sat || quantifiers ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH); options::simplificationMode.set(qf_sat ? SIMPLIFICATION_MODE_NONE : SIMPLIFICATION_MODE_BATCH); |