summaryrefslogtreecommitdiff
path: root/contrib/run-script-smtcomp2019
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/run-script-smtcomp2019')
-rwxr-xr-xcontrib/run-script-smtcomp20195
1 files changed, 4 insertions, 1 deletions
diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019
index 15bae8d0d..d917d9c5a 100755
--- a/contrib/run-script-smtcomp2019
+++ b/contrib/run-script-smtcomp2019
@@ -119,7 +119,10 @@ QF_ABV)
finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
;;
QF_UFBV)
- finishwith --bitblast=eager --bv-sat-solver=cadical
+ # Benchmarks with uninterpreted sorts cannot be solved with eager
+ # bit-blasting currently
+ trywith 2400 --bitblast=eager --bv-sat-solver=cadical
+ finishwith
;;
QF_BV)
finishwith --bv-div-zero-const --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback