Update QF_NIA strategy (#3012)

diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019
index 4138decd644f219c42e41e18fc2c5d1455a99826..d2578345385a0728b07416d13ceaa135dbadccfd 100644 (file)
--- 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