changed option to run inequality solver by default

diff --git a/src/theory/bv/options b/src/theory/bv/options
index cdc02c9adcf530ec2f166ef45db538c2a8ff54d3..2e53b029c64b9d404ed73fa15546b66c67185896 100644 (file)
--- a/src/theory/bv/options
+++ b/src/theory/bv/options
@@ -14,7 +14,7 @@ option bitvectorShareLemmas --bitblast-share-lemmas bool
 option bitvectorEagerFullcheck --bitblast-eager-fullcheck bool
  check the bitblasting eagerly
 
-option bitvectorInequalitySolver --bv-inequality-solver bool
+option bitvectorInequalitySolver --bv-inequality-solver bool :default true
  turn on the inequality solver for the bit-vector theory 
 
 option bitvectorCoreSolver --bv-core-solver bool