Updated CASC scripts, as provided to Geoff Sutcliffe

diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt
index 2a10c53477c8143de3b26d8191ad7804a680543d..b10d7324a61abca641a0413f490448c62dda72b8 100755 (executable)
--- a/contrib/run-script-casc24-fnt
+++ b/contrib/run-script-casc24-fnt
@@ -16,18 +16,18 @@ function trywith {
   (ulimit -t "$limit";$cvc4 -L tptp --szs-compliant --no-checking --no-interactive --dump-models --produce-models "$@" $bench) 2>/dev/null |
   (read result;
   case "$result" in
-    sat) echo "% SZS Satisfiable for $filename";
-         echo "% SZS output start FiniteModel for $filename";
+    sat) echo "% SZS status" "Satisfiable for $filename";
+         echo "% SZS output" "start FiniteModel for $filename";
          cat;
-         echo "% SZS output end FiniteModel for $filename";
+         echo "% SZS output" "end FiniteModel for $filename";
          exit 0;;
-    unsat) echo "% SZS Unsatisfiable for $filename"; exit 0;;
-    conjecture-sat) echo "% SZS CounterSatisfiable for $filename";
-                    echo "% SZS output start FiniteModel for $filename";
+    unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename";
+                    echo "% SZS output" "start FiniteModel for $filename";
                     cat;
-                    echo "% SZS output end FiniteModel for $filename";
+                    echo "% SZS output" "end FiniteModel for $filename";
                     exit 0;;
-    conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;;
+    conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;;
   esac; exit 1)
   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
 }
@@ -35,4 +35,4 @@ function trywith {
 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
+echo "% SZS status" "GaveUp for $filename"

diff --git a/contrib/run-script-casc24-fnt-no-models b/contrib/run-script-casc24-fnt-no-models
index a189c10bde920ff44635f3fc956cb530e6add445..3b4d5e3201f82c8016deede57fa361bcdd76edf8 100755 (executable)
--- a/contrib/run-script-casc24-fnt-no-models
+++ b/contrib/run-script-casc24-fnt-no-models
@@ -14,23 +14,23 @@ filename=${file%.*}
 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;;
+    sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;;
+    unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;;
+    conjecture-unsat) echo "% SZS status" "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;;
+    sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;;
+    unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;;
+    conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;;
   esac
 }
 
 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
+echo "% SZS status" "GaveUp for $filename"

diff --git a/contrib/run-script-casc24-fof b/contrib/run-script-casc24-fof
index 940e26946468a798a2753088eaf44083489eff6b..b3ede0dfaa37e892f9da93075ccd9a547b1a470b 100755 (executable)
--- a/contrib/run-script-casc24-fof
+++ b/contrib/run-script-casc24-fof
@@ -14,19 +14,19 @@ filename=${file%.*}
 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;;
+    sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;;
+    unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;;
+    conjecture-unsat) echo "% SZS status" "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;;
+    sat) echo "% SZS status" "Satisfiable for $filename"; exit 0;;
+    unsat) echo "% SZS status" "Unsatisfiable for $filename"; exit 0;;
+    conjecture-sat) echo "% SZS status" "CounterSatisfiable for $filename"; exit 0;;
+    conjecture-unsat) echo "% SZS status" "Theorem for $filename"; exit 0;;
   esac
 }
 
@@ -34,4 +34,4 @@ 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
+echo "% SZS status" "GaveUp for $filename"