final updates for smt-eval script

diff --git a/contrib/run-script-smteval2013 b/contrib/run-script-smteval2013
index fbdf4e039b2612729f2dcf85d600b71982780501..2212f71c799a755d7c50d964f1eab2bc339fc9c1 100755 (executable)
--- a/contrib/run-script-smteval2013
+++ b/contrib/run-script-smteval2013
@@ -27,13 +27,16 @@ case "$logic" in
 QF_LRA)
   finishwith --no-restrict-pivots --enable-miplib-trick --miplib-trick-subs=2 --fc-penalties --collect-pivot-stats --use-soi --new-prop --dio-decomps --unconstrained-simp --fancy-final
   ;;
-AUFLIA)
+AUFLIA|AUFLIRA|AUFNIRA|UFLRA|UFNIA)
   # 60 seconds with default decision heuristic
-  trywith --tlimit-per=60000
+  trywith --simplification=none --tlimit-per=60000
   # try simplification for 60 seconds, default decision heuristic
-  trywith --simplification=batch --tlimit-per=60000
+  trywith --tlimit-per=60000
   # switch to internal decision heuristic
-  finishwith --decision=internal
+  finishwith --simplification=none --decision=internal
+  ;;
+LRA)
+  finishwith --enable-cbqi
   ;;
 QF_AUFBV)
   trywith --tlimit-per=600000

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 75cffefc25683d5d419035430730d89787d3c872..0bfc6e63453f38296955855f64d8567676bf9c2b 100644 (file)
--- 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);