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-fnt | |
parent | 3b49d2e6938fbee46737bbd71419febca2ec318d (diff) |
Add option to avoid dumping partial models/proofs.
Diffstat (limited to 'contrib/run-script-cascj7-fnt')
-rwxr-xr-x | contrib/run-script-cascj7-fnt | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/run-script-cascj7-fnt b/contrib/run-script-cascj7-fnt index 9e754ffc7..ce54fe5ae 100755 --- a/contrib/run-script-cascj7-fnt +++ b/contrib/run-script-cascj7-fnt @@ -15,7 +15,7 @@ echo "------- cvc4-fnt casc j7 : $bench at $2..." 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-models --produce-models --force-no-limit-cpu-while-dump "$@" $bench) 2>/dev/null | (read w1 w2 w3 result w4 w5; case "$result" in Satisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;; @@ -25,12 +25,12 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --no-checking --no-interactive --dump-models --produce-models "$@" $bench + $cvc4 --no-checking --no-interactive --dump-models --produce-models --force-no-limit-cpu-while-dump "$@" $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 30 --finite-model-find --mbqi=abs --pre-skolem-quant --sort-inference --uf-ss-fair +trywith 15 --finite-model-find --disable-uf-ss-min-model --sort-inference --uf-ss-fair +trywith 60 --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" |