diff options
Diffstat (limited to 'contrib/run-script-smtcomp2017')
| -rw-r--r-- | contrib/run-script-smtcomp2017 | 25 |
1 files changed, 13 insertions, 12 deletions
diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017 index bb3425d91..8a0ff92ea 100644 --- a/contrib/run-script-smtcomp2017 +++ b/contrib/run-script-smtcomp2017 @@ -81,22 +81,23 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA) # finish 9min finishwith --full-saturate-quant ;; -UFBV) +BV|UFBV) # many problems in UFBV are essentially BV - trywith 300 --full-saturate-quant - trywith 300 --finite-model-find - finishwith --cbqi-all --full-saturate-quant + trywith 30 --full-saturate-quant + trywith 30 --finite-model-find + finishwith --full-saturate-quant --decision=internal ;; -BV) - trywith 300 --finite-model-find - finishwith --cbqi-all --full-saturate-quant +LIA|LRA) + trywith 30 --full-saturate-quant + trywith 300 --full-saturate-quant --cbqi-midpoint + trywith 300 --full-saturate-quant --cbqi-nested-qe + finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal ;; -LIA|LRA|NIA|NRA) +NIA|NRA) trywith 30 --full-saturate-quant - trywith 300 --full-saturate-quant --cbqi-min-bounds - trywith 300 --full-saturate-quant --decision=internal - trywith 1800 --full-saturate-quant --cbqi-nested-qe - finishwith --full-saturate-quant --cbqi-midpoint + trywith 300 --full-saturate-quant --nl-ext + trywith 300 --full-saturate-quant --cbqi-nested-qe + finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal ;; QF_AUFBV) trywith 600 |