1 files changed, 6 insertions, 6 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current
index ecc6ce5fe..9b4f534b0 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-cvc5=./cvc5
+cvc5=$(dirname "$(readlink -f "$0")")/cvc5
 bench="$1"
 
 # Output other than "sat"/"unsat" is either written to stderr or to "err.log"
@@ -75,7 +75,7 @@ QF_NRA)
   finishwith --decision=internal --nl-ext=none
   ;;
 # all logics with UF + quantifiers should either fall under this or special cases below
-ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|UFFPDTLIRA|UFFPDTNIRA)
+ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBVLIA|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBV|AUFBVDTLIA|AUFBVFP|AUFNIA|UFFPDTLIRA|UFFPDTNIRA)
   # initial runs 1 min
   trywith 30 --simplification=none --full-saturate-quant
   trywith 30 --no-e-matching --full-saturate-quant
@@ -112,7 +112,7 @@ UFBV)
   trywith 30 --full-saturate-quant --no-cegqi-innermost --global-negate
   finishwith --finite-model-find
   ;;
-BV)
+ABV|BV)
   trywith 120 --full-saturate-quant
   trywith 120 --sygus-inst
   trywith 300 --full-saturate-quant --cegqi-nested-qe --decision=internal
@@ -121,7 +121,7 @@ BV)
   # finish 10min
   finishwith --full-saturate-quant --no-cegqi-innermost --global-negate
   ;;
-ABVFP|BVFP|FP|NIA|NRA)
+ABVFP|ABVFPLRA|BVFP|FP|NIA|NRA)
   trywith 300 --full-saturate-quant --nl-ext-tplanes --fp-exp
   finishwith --sygus-inst --fp-exp
   ;;
@@ -131,8 +131,8 @@ LIA|LRA)
   finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
   ;;
 QF_AUFBV)
-  trywith 600 --ite-simp
-  finishwith --decision=justification-stoponly --ite-simp
+  trywith 600
+  finishwith --decision=justification-stoponly
   ;;
 QF_ABV)
   trywith 50 --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv