summaryrefslogtreecommitdiff
path: root/contrib
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2017-05-31 15:51:35 -0500
committerajreynol <andrew.j.reynolds@gmail.com>2017-05-31 15:51:40 -0500
commit73a60e60a6036f635e8819c672c227156b351964 (patch)
tree7a6693b16d956eb8c676d453b0a289f4be94420b /contrib
parentd121faf54238a0859cdc2cf1d3d2889631cbfa3a (diff)
Fix model construction for BV with cbqi. Minor change to defaults.
Diffstat (limited to 'contrib')
-rw-r--r--contrib/run-script-smtcomp20176
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback