Merging in bvprop branch, with proper bit-vector propagation.

This should also fix bug 325. 

1 files changed, 12 insertions, 0 deletions

diff --git a/src/util/options.h b/src/util/options.h
index 6205c7543..eac09fabf 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -283,6 +283,18 @@ struct CVC4_PUBLIC Options {
   /** Filter depending on length of lemma */
   int sharingFilterByLength;
 
+  /** Bitblast eagerly to the main sat solver */
+  bool bitvector_eager_bitblast;
+
+  /** Fullcheck at each check */
+  bool bitvector_eager_fullcheck;
+
+  /** Bitblast eagerly to the main sat solver */
+  bool bitvector_share_lemmas;
+
+  /** Refine conflicts by doing another full check after a conflict */
+  bool sat_refine_conflicts;
+
   Options();
 
   /**