diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2021-06-22 18:01:22 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-22 18:01:22 -0700 |
| commit | 474faec211db41b626ed29d8dde26ff861f40d87 (patch) | |
| tree | 3c5e68fb24113fca9e74c002614a388698d9a5f5 /contrib/competitions/smt-comp/run-script-smtcomp-current | |
| parent | 0bb3e14b46a4b2f5cacfadb313c947da73ba7df6 (diff) | |
| parent | 21ee0f18c288d430d08c133f601173be25411187 (diff) | |
Merge branch 'master' into rmTearDownIncrementalrmTearDownIncremental
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 |