diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-01 12:38:33 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-06-01 12:38:33 -0500 |
| commit | 029fb0427b59cc5251767fff902764eb4bba3771 (patch) | |
| tree | 97ef5e9f00bd2734f242a2b0855a0b52036eded0 /contrib | |
| parent | 73a60e60a6036f635e8819c672c227156b351964 (diff) | |
Minor optimizations related to cbqi.
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/run-script-smtcomp2017 | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017 index 1a9f2400f..6a0ef54b2 100644 --- a/contrib/run-script-smtcomp2017 +++ b/contrib/run-script-smtcomp2017 @@ -81,23 +81,27 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA) # finish 9min finishwith --full-saturate-quant ;; -BV|UFBV) +UFBV) # many problems in UFBV are essentially BV trywith 300 --full-saturate-quant - trywith 300 --finite-model-find + trywith 300 --full-saturate-quant --cbqi --decision=internal + finishwith --finite-model-find + ;; +BV) + trywith 300 --full-saturate-quant finishwith --full-saturate-quant --cbqi --decision=internal ;; 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 --cbqi-nested-qe --decision=internal + finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal ;; NIA|NRA) trywith 30 --full-saturate-quant trywith 300 --full-saturate-quant --nl-ext trywith 300 --full-saturate-quant --cbqi-nested-qe - finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal + finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal ;; QF_AUFBV) trywith 600 |