From 16ade2e20b6fd2afc49b8ea70d128ae665dff409 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <noetzli@stanford.edu>
Date: Mon, 20 May 2019 11:24:31 -0700
Subject: [PATCH] [SMT-COMP 2019] Update run scripts to match tracks (#3018)

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.
---
 contrib/run-script-smtcomp2019                |  0
 ...ion => run-script-smtcomp2019-incremental} |  2 +-
 .../run-script-smtcomp2019-model-validation   | 25 +++++++++++++++++++
 contrib/run-script-smtcomp2019-unsat-cores    |  0
 4 files changed, 26 insertions(+), 1 deletion(-)
 mode change 100644 => 100755 contrib/run-script-smtcomp2019
 rename contrib/{run-script-smtcomp2019-application => run-script-smtcomp2019-incremental} (98%)
 create mode 100755 contrib/run-script-smtcomp2019-model-validation
 mode change 100644 => 100755 contrib/run-script-smtcomp2019-unsat-cores

diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019
old mode 100644
new mode 100755
diff --git a/contrib/run-script-smtcomp2019-application b/contrib/run-script-smtcomp2019-incremental
similarity index 98%
rename from contrib/run-script-smtcomp2019-application
rename to contrib/run-script-smtcomp2019-incremental
index a7d4d985c..12c91a036 100755
--- a/contrib/run-script-smtcomp2019-application
+++ b/contrib/run-script-smtcomp2019-incremental
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-cvc4=./cvc4-application
+cvc4=./cvc4
 
 line=""
 while [[ -z "$line" ]]; do
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
+
diff --git a/contrib/run-script-smtcomp2019-unsat-cores b/contrib/run-script-smtcomp2019-unsat-cores
old mode 100644
new mode 100755
-- 
2.30.2