Minor updates/fix to --cbqi-recurse

1 files changed, 12 insertions, 5 deletions

diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof
index eb0478e24..582a14952 100755
--- a/contrib/run-script-cascj7-fof
+++ b/contrib/run-script-cascj7-fof
@@ -2,14 +2,15 @@
 
 cvc4=cvc4
 bench="$1"
-let "to = $2 - 85"
 
 file=${bench##*/}
 filename=${file%.*}
 
+echo "------- cvc4-fof $bench at $2..."
+
 # use: trywith [params..]
-# to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in
-# which case this run script terminates immediately.  Otherwise, this
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
 # function returns normally.
 function trywith {
   limit=$1; shift;
@@ -22,10 +23,16 @@ function trywith {
   esac; exit 1)
   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
 }
+function finishwith {
+  echo "--- Run $@ at $limit...";
+  $cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench
+}
 
 trywith 30 --full-saturate-quant
-trywith 10 --decision=internal --full-saturate-quant
+trywith 15 --decision=internal --full-saturate-quant
 trywith 30 --finite-model-find --fmf-inst-engine --mbqi=gen-ev
+trywith 30 --relevant-triggers --full-saturate-quant
 trywith 15 --finite-model-find --decision=justification-stoponly
-trywith $to --quant-cf --full-saturate-quant
+trywith 30 --pre-skolem-quant --full-saturate-quant
+finishwith --quant-cf --full-saturate-quant
 echo "% SZS status" "GaveUp for $filename"