From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Wed, 30 May 2018 18:17:35 +0000 (-0700)
Subject: Use CaDiCaL for eager bit-blasting in QF_NIA and QF_UFBV. (#2018)
X-Git-Tag: cvc5-1.0.0~4997
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c32348d5527a92894da44848297079a2797e6590;p=cvc5.git

Use CaDiCaL for eager bit-blasting in QF_NIA and QF_UFBV. (#2018)
---

diff --git a/contrib/run-script-smtcomp2018 b/contrib/run-script-smtcomp2018
index 6034fb83b..c44c81235 100644
--- a/contrib/run-script-smtcomp2018
+++ b/contrib/run-script-smtcomp2018
@@ -37,11 +37,11 @@ QF_NIA)
   trywith 300 --nl-ext-tplanes --decision=internal
   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=cryptominisat
-  trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cryptominisat
-  trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cryptominisat
-  trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cryptominisat
-  finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cryptominisat
+  trywith 300 --solve-int-as-bv=2 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig
+  trywith 300 --solve-int-as-bv=4 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig
+  trywith 300 --solve-int-as-bv=8 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig
+  trywith 300 --solve-int-as-bv=16 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig
+  finishwith --solve-int-as-bv=32 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig
   ;;
 QF_NRA)
   trywith 300 --nl-ext-tplanes --decision=internal
@@ -113,7 +113,7 @@ QF_ABV)
   finishwith --ite-simp --simp-with-care --repeat-simp --arrays-weak-equiv
   ;;
 QF_UFBV)
-  finishwith --bitblast=eager --bv-sat-solver=cryptominisat
+  finishwith --bitblast=eager --bv-sat-solver=cadical
   ;;
 QF_BV)
   finishwith --unconstrained-simp --bv-div-zero-const --bv-intro-pow2 --bitblast=eager --bv-sat-solver=cadical --bitblast-aig --bv-abstraction --bv-eq-slicer=auto