diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-06-04 12:30:28 -0700 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-06-04 14:30:28 -0500 |
| commit | cd170ce1ce9883aac0ed4ccadd85b66111d14bed (patch) | |
| tree | 2df7e8e02c4c5e361fb6037c7002155cb95573f2 /contrib/run-script-smtcomp2018 | |
| parent | db491e2e8100101f30e3f211a3c5da55686f7d27 (diff) | |
[SMT-COMP] Add new logics to run-scripts (#2022)
Diffstat (limited to 'contrib/run-script-smtcomp2018')
| -rw-r--r-- | contrib/run-script-smtcomp2018 | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018 index 6bcc5f3d3..ff06fb933 100644 --- a/contrib/run-script-smtcomp2018 +++ b/contrib/run-script-smtcomp2018 @@ -51,7 +51,7 @@ QF_NRA) finishwith --nl-ext-tplanes --decision=justification ;; # 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) +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA) # the following is designed for a run time of 20 min. # initial runs 1min trywith 30 --simplification=none --full-saturate-quant @@ -82,6 +82,9 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUF trywith 240 --finite-model-find --decision=internal finishwith --full-saturate-quant ;; +ABVFP|BVFP|FP) + finishwith --full-saturate-quant + ;; UFBV) # most problems in UFBV are essentially BV trywith 300 --full-saturate-quant --decision=internal @@ -136,6 +139,15 @@ QF_SLIA) trywith 500 --strings-exp --rewrite-divk --lang=smt2.6.1 finishwith --strings-exp --rewrite-divk --lang=smt2.6.1 --strings-fmf ;; +QF_ABVFP) + finishwith + ;; +QF_BVFP) + finishwith + ;; +QF_FP) + finishwith + ;; *) # just run the default finishwith |