From b48a369333f077fa7cce117976f760cd6332691a Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 14 May 2013 16:42:23 -0500
Subject: [PATCH] Update casc24-fnt run script.  Add casc24-fof run script.

---
 contrib/run-script-casc24-fnt |  7 ++++---
 contrib/run-script-casc24-fof | 37 +++++++++++++++++++++++++++++++++++
 2 files changed, 41 insertions(+), 3 deletions(-)
 create mode 100755 contrib/run-script-casc24-fof

diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt
index c53ac4be9..5376bfd72 100755
--- a/contrib/run-script-casc24-fnt
+++ b/contrib/run-script-casc24-fnt
@@ -2,6 +2,7 @@
 
 cvc4=./cvc4
 bench="$1"
+let "to = $2 - 60"
 
 file=${bench##*/}
 filename=${file%.*}
@@ -29,7 +30,7 @@ function finishwith {
   esac
 }
 
-trywith 15 --finite-model-find --uf-ss-totality
-trywith 15 --finite-model-find --decision=justification --fmf-fmc
-finishwith --finite-model-find --decision=justification
+trywith 30 --finite-model-find --uf-ss-totality
+trywith 30 --finite-model-find --decision=justification --fmf-fmc
+trywith $to --finite-model-find --decision=justification
 echo "SZS GaveUp for $filename"
\ No newline at end of file
diff --git a/contrib/run-script-casc24-fof b/contrib/run-script-casc24-fof
new file mode 100755
index 000000000..eb8e91310
--- /dev/null
+++ b/contrib/run-script-casc24-fof
@@ -0,0 +1,37 @@
+#!/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
-- 
2.30.2