diff options
Diffstat (limited to 'contrib/run-script-smtcomp2018-unsat-cores')
| -rw-r--r-- | contrib/run-script-smtcomp2018-unsat-cores | 11 |
1 files changed, 10 insertions, 1 deletions
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 |