diff options
Diffstat (limited to 'contrib/competitions/smt-comp/run-script-smtcomp-current')
-rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current | 12 |
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 |