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.

5 files changed, 42 insertions, 34 deletions

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index a8c6b0ba4..4c781d47c 100755
--- 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 15b95deb0..0371d8b42 100755
--- 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 27d06e104..fbc5821ce 100644
--- 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 36b2718a3..e3c14126a 100644
--- 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
index 000000000..94b484bce
--- /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)