+#!/bin/bash
+
+cvc4=./cvc4
+bench="$1"
+let "to = $2 - 75"
+
+file=${bench##*/}
+filename=${file%.*}
+
+# use: trywith [params..]
+# to attempt a run. Only thing printed on stdout is "sat" or "unsat", in
+# which case this run script terminates immediately. Otherwise, this
+# function returns normally.
+function trywith {
+ result="$( ulimit -t "$1";shift;$cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
+ case "$result" in
+ sat) echo "SZS Satisfiable for $filename"; exit 0;;
+ unsat) echo "SZS Unsatisfiable for $filename"; exit 0;;
+ conjecture-sat) echo "SZS CounterSatisfiable for $filename"; exit 0;;
+ conjecture-unsat) echo "SZS Theorem for $filename"; exit 0;;
+ esac
+}
+function finishwith {
+ result="$( $cvc4 -L tptp --szs-compliant --no-checking --no-interactive "$@" $bench)"
+ case "$result" in
+ sat) echo "SZS Satisfiable for $filename"; exit 0;;
+ unsat) echo "SZS Unsatisfiable for $filename"; exit 0;;
+ conjecture-sat) echo "SZS CounterSatisfiable for $filename"; exit 0;;
+ conjecture-unsat) echo "SZS Theorem for $filename"; exit 0;;
+ esac
+}
+
+trywith 30
+trywith 15 --finite-model-find --fmf-inst-engine
+trywith 30 --finite-model-find --decision=justification --fmf-fmc
+trywith $to --decision=justification
+echo "SZS GaveUp for $filename"
\ No newline at end of file