diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-31 11:11:02 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-31 11:11:22 -0500 |
| commit | 8fdc49e1bc53fb99050c3c46b9a8ba8541cf851b (patch) | |
| tree | 532ae530f41e22437b6b847ee57b99547a662707 /contrib | |
| parent | 61623d7bfb05143e52013db3610b63d632e61d92 (diff) | |
Minor change to defaults, update smt comp script, minor changes to options in regressions.
Diffstat (limited to 'contrib')
| -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 |