Possible final version of run scripts for casc.

[cvc5.git] / contrib / run-script-casc24-fnt

diff --git a/contrib/run-script-casc24-fnt b/contrib/run-script-casc24-fnt
index 5376bfd724fc72b97c86c10f46eb43be667da789..2a10c53477c8143de3b26d8191ad7804a680543d 100755 (executable)
--- a/contrib/run-script-casc24-fnt
+++ b/contrib/run-script-casc24-fnt
@@ -12,25 +12,27 @@ filename=${file%.*}
 # 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)"
+  limit=$1; shift;
+  (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"; 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
+    sat) echo "% SZS Satisfiable for $filename";
+         echo "% SZS output start FiniteModel for $filename";
+         cat;
+         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";
+                    cat;
+                    echo "% SZS output end FiniteModel for $filename";
+                    exit 0;;
+    conjecture-unsat) echo "% SZS Theorem for $filename"; exit 0;;
+  esac; exit 1)
+  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
 }
 
 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 GaveUp for $filename"
\ No newline at end of file