diff options
| author | Andres Noetzli <noetzli@stanford.edu> | 2021-06-08 11:13:07 -0700 |
|---|---|---|
| committer | Andres Noetzli <noetzli@stanford.edu> | 2021-06-08 11:13:07 -0700 |
| commit | f126944cb2b594df2a40782310fd8a0090175a45 (patch) | |
| tree | d6e27d20de922e052b2a6b36374a12313a67cc9c | |
| parent | b88356df2d0092046c43692213f94b7bb5cc7965 (diff) | |
update
| -rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index 77ce65bab..6e1c7fb99 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -58,15 +58,15 @@ QF_LIA) QF_NIA) trywith 420 --nl-ext-tplanes --decision=justification trywith 60 --nl-ext-tplanes --decision=internal - trywith 60 --nl-ext-tplanes --decision=justification + trywith 60 --nl-ext-tplanes --decision=justification-old trywith 60 --no-nl-ext-tplanes --decision=internal trywith 60 --no-arith-brab --nl-ext-tplanes --decision=internal # this totals up to more than 20 minutes, although notice that smaller bit-widths may quickly fail - trywith 300 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction - trywith 600 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + trywith 300 --solve-int-as-bv=2 --bitblast=eager + trywith 300 --solve-int-as-bv=4 --bitblast=eager + trywith 300 --solve-int-as-bv=8 --bitblast=eager + trywith 300 --solve-int-as-bv=16 --bitblast=eager + trywith 600 --solve-int-as-bv=32 --bitblast=eager finishwith --nl-ext-tplanes --decision=internal ;; QF_NRA) |