Update casc and sygus comp scripts.

1 files changed, 22 insertions, 5 deletions

diff --git a/contrib/run-script-sygusComp2017-INV b/contrib/run-script-sygusComp2017-INV
index a25a5f5c8..a21792fb9 100755
--- a/contrib/run-script-sygusComp2017-INV
+++ b/contrib/run-script-sygusComp2017-INV
@@ -3,14 +3,31 @@
 cvc4=./cvc4
 bench="$1"
 
+function runl {
+  limit=$1; shift;
+  ulimit -S -t "$limit";$cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench
+}
+
 function trywith {
-  ($cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench) 2>/dev/null |
+  sol=$(runl $@)
+  status=$?
+  if [ $status -ne 134 ]; then
+    echo $sol |
+    (read result w1;
+    case "$result" in
+    unsat) echo "$w1";cat;exit 0;;
+    esac; exit 1)
+    if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi  
+  fi
+}
+
+function finishwith {
+  $cvc4 --lang=sygus --no-checking --no-interactive --dump-synth --default-dag-thresh=0 "$@" $bench 2>/dev/null |
   (read result w1;
   case "$result" in
   unsat) echo "$w1";cat;exit 0;;
-  esac; exit 1)
-  if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
+  esac)
 }
 
-trywith --sygus-inv-templ=post
- 
+trywith 60 --sygus-inv-templ=pre
+finishwith --sygus-inv-templ=post