[SMT-COMP 2019] Update run scripts to match tracksupdateRunScripts

The "Application Track" has been renamed to "Incremental Track" this
year, so this commit renames the script accordingly and updates the name
of the CVC4 binary that the script calls to be just `cvc4`. The commit
also adds an initial script for the model validation track.

1 files changed, 25 insertions, 0 deletions

diff --git a/contrib/run-script-smtcomp2019-model-validation b/contrib/run-script-smtcomp2019-model-validation
new file mode 100755
index 000000000..f4b812fd6
--- /dev/null
+++ b/contrib/run-script-smtcomp2019-model-validation
@@ -0,0 +1,25 @@
+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+
+logic=$(expr "$(grep -m1 '^[^;]*set-logic' "$bench")" : ' *(set-logic  *\([A-Z_]*\) *) *$')
+
+# use: finishwith [params..]
+# to run cvc4 and let it output whatever it will to stdout.
+function finishwith {
+  $cvc4 -L smt2.6 --no-incremental --no-checking --no-interactive "$@" $bench
+}
+
+case "$logic" in
+
+QF_BV)
+  finishwith --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cadical --bv-eq-slicer=auto --no-bv-abstraction
+  ;;
+*)
+  # just run the default
+  finishwith
+  ;;
+
+esac
+