diff options
-rw-r--r-- | contrib/run-script-smtcomp2018 | 14 | ||||
-rwxr-xr-x | contrib/run-script-smtcomp2018-application | 27 | ||||
-rw-r--r-- | contrib/run-script-smtcomp2018-unsat-cores | 11 |
3 files changed, 50 insertions, 2 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 diff --git a/contrib/run-script-smtcomp2018-application b/contrib/run-script-smtcomp2018-application index 4bf2f6b91..58db84d36 100755 --- a/contrib/run-script-smtcomp2018-application +++ b/contrib/run-script-smtcomp2018-application @@ -49,6 +49,33 @@ QF_BV) QF_LIA) runcvc4 --tear-down-incremental=1 --unconstrained-simp ;; +QF_UFBV) + runcvc4 --incremental + ;; +QF_UF) + runcvc4 --incremental + ;; +QF_AUFBV) + runcvc4 --incremental + ;; +QF_ABV) + runcvc4 --incremental + ;; +ABVFP) + runcvc4 --incremental + ;; +BVFP) + runcvc4 --incremental + ;; +QF_ABVFP) + runcvc4 --incremental + ;; +QF_BVFP) + runcvc4 --incremental + ;; +QF_FP) + runcvc4 --incremental + ;; *) # just run the default runcvc4 --incremental diff --git a/contrib/run-script-smtcomp2018-unsat-cores b/contrib/run-script-smtcomp2018-unsat-cores index 24933cf40..1454e7a8a 100644 --- a/contrib/run-script-smtcomp2018-unsat-cores +++ b/contrib/run-script-smtcomp2018-unsat-cores @@ -26,7 +26,7 @@ QF_NRA) finishwith --nl-ext --nl-ext-tplanes ;; # 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|ABVFP|BVFP|FP) finishwith --full-saturate-quant ;; UFBV) @@ -65,6 +65,15 @@ QF_AUFNIA) QF_ALIA) finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas ;; +QF_ABVFP) + finishwith + ;; +QF_BVFP) + finishwith + ;; +QF_FP) + finishwith + ;; *) # just run the default finishwith |