From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 5 Feb 2020 00:27:17 +0000 (-0600)
Subject: Fix QF_NIA smt comp script (#3715)
X-Git-Tag: cvc5-1.0.0~3679
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ea4355639142f10a2bc5c1aa6044d9bbc246435b;p=cvc5.git

Fix QF_NIA smt comp script (#3715)
---

diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
index 795de734b..15b95deb0 100755
--- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
+++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores
@@ -20,7 +20,7 @@ QF_LIA)
   finishwith --miplib-trick --miplib-trick-subs=4 --use-approx --lemmas-on-replay-failure --replay-early-close-depth=4 --replay-lemma-reject-cut=128 --replay-reject-cut=512 --use-soi
   ;;
 QF_NIA)
-  finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat
+  finishwith --nl-ext --nl-ext-tplanes
   ;;
 QF_NRA)
   finishwith --nl-ext --nl-ext-tplanes