diff options
| author | ajreynol <reynolds@laraserver2.epfl.ch> | 2014-05-28 23:32:59 +0200 |
|---|---|---|
| committer | ajreynol <reynolds@laraserver2.epfl.ch> | 2014-05-28 23:32:59 +0200 |
| commit | d38ad982be4717eee4fa102533e12c338b2d1b37 (patch) | |
| tree | 62ca2dcf4f7889bfe432563508b5e3e22e2bf3fc /contrib/run-script-cascj7-tff | |
| parent | b8bd234936a499d72cb5a9444f8cfd82d980fe8f (diff) | |
Minor changes to script. Disable cbqi sat.
Diffstat (limited to 'contrib/run-script-cascj7-tff')
| -rwxr-xr-x | contrib/run-script-cascj7-tff | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/run-script-cascj7-tff b/contrib/run-script-cascj7-tff index 5dd1a9d98..9422f8536 100755 --- a/contrib/run-script-cascj7-tff +++ b/contrib/run-script-cascj7-tff @@ -25,14 +25,14 @@ function trywith { } function finishwith { echo "--- Run $@..."; - $cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench + $cvc4 --no-checking --no-interactive "$@" $bench } 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 30 --full-saturate-quant +trywith 30 --fmf-bound-int trywith 60 --quant-cf --full-saturate-quant finishwith --cbqi-recurse --full-saturate-quant --pre-skolem-quant # echo "% SZS status" "GaveUp for $filename" |