Possible final version of run scripts for casc.

1 files changed, 9 insertions, 9 deletions

diff --git a/contrib/run-script-casc24-fof b/contrib/run-script-casc24-fof
index eb8e91310..940e26946 100755
--- 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 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;;
+    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
 }
 
@@ -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 GaveUp for $filename"
\ No newline at end of file