diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-31 15:51:35 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-05-31 15:51:40 -0500 |
commit | 73a60e60a6036f635e8819c672c227156b351964 (patch) | |
tree | 7a6693b16d956eb8c676d453b0a289f4be94420b /contrib | |
parent | d121faf54238a0859cdc2cf1d3d2889631cbfa3a (diff) |
Fix model construction for BV with cbqi. Minor change to defaults.
Diffstat (limited to 'contrib')
-rw-r--r-- | contrib/run-script-smtcomp2017 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017 index 9af6fffd0..1a9f2400f 100644 --- a/contrib/run-script-smtcomp2017 +++ b/contrib/run-script-smtcomp2017 @@ -85,19 +85,19 @@ BV|UFBV) # many problems in UFBV are essentially BV trywith 300 --full-saturate-quant trywith 300 --finite-model-find - finishwith --full-saturate-quant --decision=internal + 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-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-nested-qe --decision=internal + finishwith --full-saturate-quant --cbqi --cbqi-nested-qe --decision=internal ;; QF_AUFBV) trywith 600 |