diff options
| author | Clark Barrett <barrett@cs.nyu.edu> | 2015-06-14 13:30:54 -0700 |
|---|---|---|
| committer | Clark Barrett <barrett@cs.nyu.edu> | 2015-06-14 13:31:07 -0700 |
| commit | 3cc872041d7d0e9f525f234de53adefc23ffc5ae (patch) | |
| tree | 707c789a7e556eb178c67a0dc8f5080661ea41cc | |
| parent | 58228bd65d209ac7637676027b902fb05d3d53bf (diff) | |
More updates for QF_NIA
| -rwxr-xr-x | contrib/run-script-smtcomp2015 | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/contrib/run-script-smtcomp2015 b/contrib/run-script-smtcomp2015 index cf46cf4ec..6926e16cd 100755 --- a/contrib/run-script-smtcomp2015 +++ b/contrib/run-script-smtcomp2015 @@ -34,9 +34,12 @@ QF_LIA) finishwith --enable-miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --unconstrained-simp --use-soi --pb-rewrites ;; QF_NIA) - trywith 10 + trywith 20 + trywith 1800 --solve-int-as-bv=2 --bitblast=eager + trywith 1800 --solve-int-as-bv=4 --bitblast=eager trywith 1800 --solve-int-as-bv=8 --bitblast=eager - finishwith --solve-int-as-bv=16 --bitblast=eager + trywith 1800 --solve-int-as-bv=16 --bitblast=eager + finishwith --solve-int-as-bv=32 --bitblast=eager ;; AUFLIA) finishwith --no-e-matching --full-saturate-quant |