More preparation for CASC proofs. Minor fix for sort inference (rewrite new assertions). Bug fix for ambqi : simplify correctly for multi-sorted case. Bug fix for fmc : only do exh-simplification for uninterpreted sorts, ensure reps are enumerated for quantification over Real.

3 files changed, 14 insertions, 13 deletions

diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt
index 11133cd0f..5d51381da 100755
--- a/contrib/run-script-cascj7-fnt
+++ b/contrib/run-script-cascj7-fnt
@@ -25,8 +25,8 @@ function trywith {
   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
 }
 
-trywith 30 --finite-model-find 
-trywith 30 --finite-model-find --mbqi=gen-ev --uf-ss-totality --decision=internal
-trywith 10 --finite-model-find --disable-uf-ss-min-model
-trywith $to --finite-model-find --mbqi=abs --pre-skolem-quant
+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
 echo "% SZS status" "GaveUp for $filename"
diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof
index 151413ac2..eb0478e24 100755
--- a/contrib/run-script-cascj7-fof
+++ b/contrib/run-script-cascj7-fof
@@ -7,8 +7,6 @@ let "to = $2 - 85"
 file=${bench##*/}
 filename=${file%.*}
 
-echo "Run $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
@@ -16,7 +14,7 @@ echo "Run $bench at $2"
 function trywith {
   limit=$1; shift;
   echo "--- Run $@ at $limit...";
-  (ulimit -t "$limit";$cvc4 --no-checking --no-interactive "$@" $bench) 2>/dev/null |
+  (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench) 2>/dev/null |
   (read w1 w2 w3 result w4 w5;
   case "$result" in
   Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
diff --git a/contrib/run-script-cascj7-tff b/contrib/run-script-cascj7-tff
index 445f7b08a..893b69572 100755
--- a/contrib/run-script-cascj7-tff
+++ b/contrib/run-script-cascj7-tff
@@ -1,8 +1,8 @@
 #!/bin/bash
 
-cvc4=./cvc4
+cvc4=cvc4
 bench="$1"
-let "to = $2 - 150"
+let "to = $2 - 170"
 
 file=${bench##*/}
 filename=${file%.*}
@@ -14,7 +14,7 @@ filename=${file%.*}
 function trywith {
   limit=$1; shift;
   echo "--- Run $@ at $limit...";
-  (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-models --produce-models "$@" $bench) 2>/dev/null |
+  (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench) 2>/dev/null |
   (read w1 w2 w3 result w4 w5;
   case "$result" in
   Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
@@ -23,7 +23,10 @@ function trywith {
   if [ ${PIPESTATUS[1]} -eq 0 ]; then exit 0; fi
 }
 
-trywith 30 --full-saturate-quant
-trywith 120 --quant-cf --qcf-tconstraint --full-saturate-quant
-trywith $to --cbqi --cbqi-recurse --full-saturate-quant --flip-decision
+trywith 15 --cbqi-recurse --full-saturate-quant
+trywith 15 --decision=internal --full-saturate-quant
+trywith 30 --quant-cf --qcf-tconstraint --full-saturate-quant
+trywith 20 --finite-model-find
+trywith 90 --full-saturate-quant
+trywith $to --cbqi-recurse --full-saturate-quant --pre-skolem-quant
 echo "% SZS status" "GaveUp for $filename"