diff options
Diffstat (limited to 'contrib/run-script-casc24-fof')
-rwxr-xr-x | contrib/run-script-casc24-fof | 18 |
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 |