From: Andres Noetzli <noetzli@stanford.edu>
Date: Mon, 19 Jun 2017 06:51:27 +0000 (-0700)
Subject: Better configuration for QF_NRA
X-Git-Tag: cvc5-1.0.0~5760^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3582df14e0bc8a3783ca231c67a0469ed0161042;p=cvc5.git

Better configuration for QF_NRA
---

diff --git a/contrib/run-script-smtcomp2017 b/contrib/run-script-smtcomp2017
index b476203d5..06cd6a6e4 100644
--- a/contrib/run-script-smtcomp2017
+++ b/contrib/run-script-smtcomp2017
@@ -42,6 +42,7 @@ QF_NIA)
   finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat
   ;;
 QF_NRA)
+  trywith 300 --nl-ext --nl-ext-tplanes --decision=justification
   finishwith --nl-ext --nl-ext-tplanes
   ;;
 # all logics with UF + quantifiers should either fall under this or special cases below