Do not enable some SMT-COMP specific options by default (#4038)

Moves SMT-COMP-specific options to the SMT-COMP script. Both of these options have led to issues (segfaults or infinite loops).

Issue #789 can be downgraded to "minor" after this PR.

Btw, I did not add these specialized options to the "incremental" script of SMT-COMP, since I'm assuming they should not be used there.

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index a8c6b0ba42f7248d43bc1875e3e29e504eed307d..4c781d47cf1fd17541e321245860ab11e6909e52 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -32,7 +32,7 @@ QF_LRA)
   ;;
 QF_LIA)
   # same as QF_LRA but add --pb-rewrites
-  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites
+  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites --ite-simp --simp-ite-compress
   ;;
 QF_NIA)
   trywith 600 --nl-ext-tplanes --decision=internal
@@ -110,8 +110,8 @@ LIA|LRA|NIA|NRA)
   finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)
-  trywith 1200
-  finishwith --decision=justification-stoponly
+  trywith 1200 --ite-simp
+  finishwith --decision=justification-stoponly --ite-simp
   ;;
 QF_ABV)
   trywith 100 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
index 15b95deb0058da35b67a1d82aec9508931960c05..0371d8b4295231b7006b641c0a09cff9e1138906 100755 (executable)
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
@@ -17,7 +17,7 @@ QF_LRA)
   finishwith --no-restrict-pivots --use-soi --new-prop
   ;;
 QF_LIA)
-  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi
+  finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi --ite-simp --simp-ite-compress
   ;;
 QF_NIA)
   finishwith --nl-ext --nl-ext-tplanes
@@ -42,7 +42,7 @@ NIA|NRA)
   finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)
-  finishwith --decision=justification-stoponly
+  finishwith --decision=justification-stoponly --ite-simp
   ;;
 QF_ABV)
   finishwith --ite-simp --simp-with-care --arrays-weak-equiv

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 27d06e1042873cdfdef9d7b2307af103b19d97f1..fbc5821ce232f107179640a53a993758afe8d6ae 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1627,35 +1627,6 @@ void SmtEngine::setDefaults() {
     Theory::setUninterpretedSortOwner(THEORY_UF);
   }
 
-  // Turn on ite simplification for QF_LIA and QF_AUFBV
-  // WARNING: These checks match much more than just QF_AUFBV and
-  // QF_LIA logics. --K [2014/10/15]
-  if(! options::doITESimp.wasSetByUser()) {
-    bool qf_aufbv = !d_logic.isQuantified() &&
-      d_logic.isTheoryEnabled(THEORY_ARRAYS) &&
-      d_logic.isTheoryEnabled(THEORY_UF) &&
-      d_logic.isTheoryEnabled(THEORY_BV);
-    bool qf_lia = !d_logic.isQuantified() &&
-      d_logic.isPure(THEORY_ARITH) &&
-      d_logic.isLinear() &&
-      !d_logic.isDifferenceLogic() &&
-      !d_logic.areRealsUsed();
-
-    bool iteSimp = (qf_aufbv || qf_lia);
-    Trace("smt") << "setting ite simplification to " << iteSimp << endl;
-    options::doITESimp.set(iteSimp);
-  }
-  if(! options::compressItes.wasSetByUser() ){
-    bool qf_lia = !d_logic.isQuantified() &&
-      d_logic.isPure(THEORY_ARITH) &&
-      d_logic.isLinear() &&
-      !d_logic.isDifferenceLogic() &&
-      !d_logic.areRealsUsed();
-
-    bool compressIte = qf_lia;
-    Trace("smt") << "setting ite compression to " << compressIte << endl;
-    options::compressItes.set(compressIte);
-  }
   if(! options::simplifyWithCareEnabled.wasSetByUser() ){
     bool qf_aufbv = !d_logic.isQuantified() &&
       d_logic.isTheoryEnabled(THEORY_ARRAYS) &&

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 36b2718a3573a267a6932593a74eb041bf8f67dd..e3c14126ae89b373d67fd34b3bf64659a2667cf9 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1184,6 +1184,7 @@ set(regress_1_tests
   regress1/arith/div.08.smt2
   regress1/arith/div.09.smt2
   regress1/arith/issue3952-rew-eq.smt2
+  regress1/arith/issue789.smt2
   regress1/arith/miplib3.cvc
   regress1/arith/mod.02.smt2
   regress1/arith/mod.03.smt2

diff --git a/test/regress/regress1/arith/issue789.smt2 b/test/regress/regress1/arith/issue789.smt2
new file mode 100644 (file)
index 0000000..94b484b
--- /dev/null
+++ b/test/regress/regress1/arith/issue789.smt2
@@ -0,0 +1,36 @@
+(set-logic QF_LIA)
+(set-info :status sat)
+(declare-fun _substvar_67_ () Int)
+(declare-fun _substvar_66_ () Int)
+(declare-fun _substvar_59_ () Int)
+(declare-fun _substvar_54_ () Int)
+(declare-fun _substvar_53_ () Int)
+(declare-fun _substvar_65_ () Int)
+(declare-fun _substvar_37_ () Int)
+(declare-fun _substvar_40_ () Int)
+(declare-fun _substvar_38_ () Int)
+(declare-fun _substvar_39_ () Int)
+(declare-fun _substvar_60_ () Int)
+(declare-fun _substvar_70_ () Int)
+(declare-fun x4 () Int)
+(declare-fun x13 () Int)
+(declare-fun x3 () Int)
+(declare-fun x18 () Int)
+(declare-fun x7 () Int)
+(declare-fun x15 () Int)
+(declare-fun x9 () Int)
+(declare-fun x1 () Int)
+(declare-fun x17 () Int)
+(declare-fun x16 () Int)
+(declare-fun x8 () Int)
+(declare-fun x19 () Int)
+(declare-fun x2 () Int)
+(declare-fun x12 () Int)
+(declare-fun x10 () Int)
+(declare-fun x6 () Int)
+(declare-fun x14 () Int)
+(declare-fun x11 () Int)
+(declare-fun x5 () Int)
+(assert (let ( (x23 (* _substvar_37_ 2)) (x24 false)) (let ((x26 false) (x25 (not false))) (let ((x29 (= 0 0)) (x30 false) (x27 (not false)) (x28 false)) (let ((x34 false) (x37 (>= _substvar_37_ 8)) (x33 false) (x36 (= 0 (+ x23 0))) (x32 (= 16 _substvar_60_)) (x38 (+ x23 (- _substvar_67_))) (x35 (= 0 _substvar_67_))) (let ((x39 (= x38 16)) (x40 false)) (let ((x43 (= _substvar_53_ 16))) (let ((x45 false) (x46 false)) (let ((x49 (= 0 0)) (x48 false) (x47 (not false))) (and (and (and (and (and (and (or false x27) (and (or false x32) (and (and (or (not false) false) (and (or x49 false) (and (or x43 false) (and (and (and (or x36 x35) (and (and (and (and (or false x25) (or false x39)) (or x39 false)) (or x36 x37)) (or x35 (not x37)))) (or x43 false)) (or false x47))))) (or false x49)))) (or false x32)) (or x29 false)) (or (not false) false)) (or x29 false)) (and (and (and (and (<= 0 0) (not false)) (and (and (= false false) (and (and (and (<= 0 0) (not false)) (and (and (and (not false) (>= 0 0)) (and (and (<= 0 1) (>= 0 0)) (and (and (and (>= 0 0) x47) (and (and (>= 1 0) (<= 0 0)) (and (and (and (and (= false false) (and (and (>= 0 0) (not false)) (and (and (= false false) (and (and (>= 0 0) (not false)) (and (and (and (and (not false) (>= 0 0)) (and (and (= false false) (and (and (and (>= 1 0) (>= 0 0)) (and (and (and (not false) (>= 0 0)) (and (and (>= 0 0) (not false)) (and (<= 0 0) x27))) (and (<= 0 _substvar_37_) x25))) (and (<= 0 0) (not false)))) (and (>= 0 0) (not false)))) (= false false)) (and (not false) (>= 0 0))))) (and (<= 0 0) (>= 1 0))))) (and (>= 0 0) (>= 1 0))) (and (>= 0 0) (not (<= 16 0)))) (= false false)))) (= (= 1 0) (not (<= 0 16)))))) (= (not (>= 16 0)) (= 0 1)))) (and (not (>= 0 8)) (>= 0 0)))) (and (<= 0 0) (<= 0 1)))) (= (= 0 1) (not (>= 16 0)))) (not (= _substvar_54_ 0)))))))))))))
+(check-sat)
+(exit)