summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2018-05-30 12:49:46 -0500
committerAndres Noetzli <andres.noetzli@gmail.com>2018-05-30 10:49:46 -0700
commit3b110a7a599011deca7bececb3622507f31c3527 (patch)
tree05839c1062e1d23f98f7eded9716cb512897d3e8
parent376b087640581a935784cf7db4cf5f4ea2a34e05 (diff)
Draft run script for strings smt comp 2018. (#2016)
-rw-r--r--contrib/run-script-smtcomp20184
1 files changed, 4 insertions, 0 deletions
diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018
index 9057282e5..6034fb83b 100644
--- a/contrib/run-script-smtcomp2018
+++ b/contrib/run-script-smtcomp2018
@@ -131,6 +131,10 @@ QF_ALIA)
trywith 70 --decision=justification --arrays-weak-equiv
finishwith --decision=justification-stoponly --no-arrays-eager-index --arrays-eager-lemmas
;;
+QF_SLIA)
+ trywith 500 --strings-exp --rewrite-divk --lang=smt2.6.1
+ finishwith --strings-exp --rewrite-divk --lang=smt2.6.1 --strings-fmf
+ ;;
*)
# just run the default
finishwith
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback