From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Sat, 18 May 2019 04:07:48 +0000 (-0500)
Subject: Update QF_NIA strategy (#3012)
X-Git-Tag: cvc5-1.0.0~4141
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3d79c9b5813eda2f6f55822e193e36a660435e10;p=cvc5.git

Update QF_NIA strategy (#3012)
---

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