From 3d79c9b5813eda2f6f55822e193e36a660435e10 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 17 May 2019 23:07:48 -0500 Subject: [PATCH] Update QF_NIA strategy (#3012) --- contrib/run-script-smtcomp2019 | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019 index 4138decd6..d25783453 100644 --- a/contrib/run-script-smtcomp2019 +++ b/contrib/run-script-smtcomp2019 @@ -36,13 +36,15 @@ QF_LIA) ;; QF_NIA) trywith 300 --nl-ext-tplanes --decision=internal + trywith 30 --nl-ext-tplanes --decision=justification trywith 30 --no-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 --bitblast-aig --no-bv-abstraction trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction - finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction + trywith 600 --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --no-bv-abstraction + finishwith --nl-ext-tplanes --decision=internal ;; QF_NRA) trywith 300 --nl-ext-tplanes --decision=internal -- 2.30.2