From: Liana Hadarean <lianahady@gmail.com>
Date: Sun, 31 Mar 2013 03:47:03 +0000 (-0400)
Subject: changed option to run inequality solver by default
X-Git-Tag: cvc5-1.0.0~7357
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d803fada76b1c45c3da6960865fdc8d061c7b680;p=cvc5.git

changed option to run inequality solver by default
---

diff --git a/src/theory/bv/options b/src/theory/bv/options
index cdc02c9ad..2e53b029c 100644
--- 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