diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-02 15:54:14 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-02 15:54:14 -0500 |
| commit | 04db70f9a8b5a4dd28e6bba893ea327536f3e91f (patch) | |
| tree | fe2a28bc9a373a79dda7d4cb03cd4c5d9bf5171d /contrib | |
| parent | 029fb0427b59cc5251767fff902764eb4bba3771 (diff) | |
Incorporate datatypes into smt comp script, add regression.
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/run-script-smtcomp2017 | 31 |
1 files changed, 15 insertions, 16 deletions
diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017 index 6a0ef54b2..ffa54bec9 100644 --- a/contrib/run-script-smtcomp2017 +++ b/contrib/run-script-smtcomp2017 @@ -44,45 +44,44 @@ QF_NIA) QF_NRA) finishwith --nl-ext --nl-ext-tplanes ;; -ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA) +# 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) # the following is designed for a run time of 2400s (40 min). # initial runs 1min trywith 20 --simplification=none --full-saturate-quant trywith 20 --no-e-matching --full-saturate-quant trywith 20 --fs-inst --decision=internal --full-saturate-quant - # trigger selections 4min + # trigger selections 3min trywith 30 --relevant-triggers --full-saturate-quant trywith 30 --trigger-sel=max --full-saturate-quant - trywith 30 --trigger-sel=min-s-max --full-saturate-quant trywith 30 --multi-trigger-when-single --full-saturate-quant trywith 30 --multi-trigger-when-single --multi-trigger-priority --full-saturate-quant trywith 30 --multi-trigger-cache --full-saturate-quant trywith 30 --no-multi-trigger-linear --full-saturate-quant - trywith 30 --literal-match=agg --full-saturate-quant # other 3min trywith 30 --pre-skolem-quant --full-saturate-quant trywith 30 --inst-when=full --full-saturate-quant - trywith 30 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant trywith 30 --no-e-matching --no-quant-cf --full-saturate-quant - trywith 60 --nl-ext --full-saturate-quant + trywith 30 --nl-ext --full-saturate-quant + trywith 60 --decision=internal --simplification=none --no-inst-no-entail --no-quant-cf --full-saturate-quant # finite model find 2min - trywith 30 --finite-model-find --mbqi=none - trywith 30 --finite-model-find - trywith 30 --finite-model-find --uf-ss=no-minimal - trywith 60 --finite-model-find --decision=internal + trywith 20 --finite-model-find --mbqi=none + trywith 20 --finite-model-find + trywith 20 --finite-model-find --uf-ss=no-minimal + trywith 60 --finite-model-find --fmf-inst-engine # long runs 20min - trywith 300 --decision=internal --full-saturate-quant - trywith 300 --term-db-mode=relevant --full-saturate-quant - trywith 300 --fs-inst --full-saturate-quant - trywith 300 --finite-model-find --fmf-inst-engine + trywith 200 --decision=internal --full-saturate-quant + trywith 200 --term-db-mode=relevant --full-saturate-quant + trywith 200 --fs-inst --full-saturate-quant + trywith 600 --finite-model-find --decision=internal # finite model find 1min trywith 30 --finite-model-find --fmf-bound-int trywith 30 --finite-model-find --sort-inference - # finish 9min + # finish 10min finishwith --full-saturate-quant ;; UFBV) - # many problems in UFBV are essentially BV + # most problems in UFBV are essentially BV trywith 300 --full-saturate-quant trywith 300 --full-saturate-quant --cbqi --decision=internal finishwith --finite-model-find |