diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-22 08:45:52 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-22 08:45:52 -0500 |
commit | 286ed8f8a3d6aece0469e983e87626a25107608d (patch) | |
tree | f710a94efc205c0333ad28d7996a8c1d00d00cc3 /contrib | |
parent | da73f99910a25fca342c0ba1d8ec19de6c3cefda (diff) |
Allow eager bitblasting with solve bv as int in QF_NIA (#4373)
This also updates the SMT COMP script to revert to our previous behavior.
This is required for SMT COMP. It should be beneficial for satisfiable QF_NIA instances. I will revisit/test this independently.
Diffstat (limited to 'contrib')
-rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index b0bc70cd7..8a1d674ed 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -39,11 +39,11 @@ QF_NIA) trywith 60 --nl-ext-tplanes --decision=justification trywith 60 --no-nl-ext-tplanes --decision=internal # this totals up to more than 40 minutes, although notice that smaller bit-widths may quickly fail - trywith 600 --solve-int-as-bv=2 --bv-sat-solver=cadical --no-bv-abstraction - trywith 600 --solve-int-as-bv=4 --bv-sat-solver=cadical --no-bv-abstraction - trywith 600 --solve-int-as-bv=8 --bv-sat-solver=cadical --no-bv-abstraction - trywith 600 --solve-int-as-bv=16 --bv-sat-solver=cadical --no-bv-abstraction - trywith 1200 --solve-int-as-bv=32 --bv-sat-solver=cadical --no-bv-abstraction + trywith 600 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + trywith 600 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + trywith 600 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + trywith 600 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction + trywith 1200 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --no-bv-abstraction finishwith --nl-ext-tplanes --decision=internal ;; QF_NRA) |