diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-28 02:28:39 -0500 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-28 02:28:39 -0500 |
| commit | b8bd234936a499d72cb5a9444f8cfd82d980fe8f (patch) | |
| tree | bd2971ad0f7a5239c89f05abba52ebe3b8da2245 /contrib/run-script-cascj7-fof | |
| parent | 3b49d2e6938fbee46737bbd71419febca2ec318d (diff) | |
Add option to avoid dumping partial models/proofs.
Diffstat (limited to 'contrib/run-script-cascj7-fof')
| -rwxr-xr-x | contrib/run-script-cascj7-fof | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof index 2e4f4d0b9..783eca17e 100755 --- a/contrib/run-script-cascj7-fof +++ b/contrib/run-script-cascj7-fof @@ -15,7 +15,7 @@ echo "------- cvc4-fof casc j7 : $bench at $2..." function trywith { limit=$1; shift; echo "--- Run $@ at $limit..."; - (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench) 2>/dev/null | + (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $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;; @@ -25,7 +25,7 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench + $cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs --force-no-limit-cpu-while-dump "$@" $bench } trywith 15 --quant-cf --pre-skolem-quant --full-saturate-quant |