diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-11 14:36:50 -0500 |
| commit | 0b2f9943d55152e0958369083649dd71340864c9 (patch) | |
| tree | cd040f1dd12816c6af37548597bd674cafb45271 /contrib/run-script-cascj7-fof | |
| parent | 8ebd49cb903ba19f9330820d02af08e226c9b791 (diff) | |
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.
Diffstat (limited to 'contrib/run-script-cascj7-fof')
| -rwxr-xr-x | contrib/run-script-cascj7-fof | 4 |
1 files changed, 1 insertions, 3 deletions
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;; |