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 6034fb83b5597e6bace3d99ea3e52c2a50ed663b..c44c81235f9d283ee0b4e5c379104c31e5737e37 100644 (file)
--- 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