Minor updates/fix to --cbqi-recurse

1 files changed, 9 insertions, 5 deletions

diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt
index 5d51381da..073a9f297 100755
--- a/contrib/run-script-cascj7-fnt
+++ b/contrib/run-script-cascj7-fnt
@@ -2,16 +2,15 @@
 
 cvc4=cvc4
 bench="$1"
-let "to = $2 - 70"
 
 file=${bench##*/}
 filename=${file%.*}
 
-echo "Run $bench at $2"
+echo "------- cvc4-fnt $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;
@@ -24,9 +23,14 @@ 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-models --produce-models "$@" $bench
+}
 
 trywith 30 --finite-model-find --sort-inference --uf-ss-fair
 trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality --decision=internal --sort-inference --uf-ss-fair
 trywith 10 --finite-model-find --disable-uf-ss-min-model --sort-inference --uf-ss-fair
-trywith $to --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair
+trywith 30 --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair
+finishwith --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair --mbqi-one-inst-per-round
 echo "% SZS status" "GaveUp for $filename"