Enable BV proofs when using an eager bitblaster (#2733)

* Enable BV proofs when using and eager bitblaster

Specifically:
   * Removed assertions that blocked them.
   * Made sure that only bitvectors were stored in the BV const let-map
   * Prevented true/false from being bit-blasted by the eager bitblaster

Also:
   * uncommented "no-check-proofs" from relevant tests

* Option handler logic for BV proofs

BV eager proofs only work when minisat is the sat solver being used by
the BV theory.

Added logic to the --proof hanlder to  verify this or throw an option
exception.

* Bugfix for proof options handler

I forgot that proofEnabledBuild runs even if the --proof option is
negated. In my handler I now check that proofs are enabled.

* Clang-format

1 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/bv/bitblast/eager_bitblaster.cpp b/src/theory/bv/bitblast/eager_bitblaster.cpp
index 33d5a1c80..019918c2f 100644
--- a/src/theory/bv/bitblast/eager_bitblaster.cpp
+++ b/src/theory/bv/bitblast/eager_bitblaster.cpp
@@ -99,8 +99,8 @@ void EagerBitblaster::bbFormula(TNode node)
 void EagerBitblaster::bbAtom(TNode node)
 {
   node = node.getKind() == kind::NOT ? node[0] : node;
-  if (node.getKind() == kind::BITVECTOR_BITOF) return;
-  if (hasBBAtom(node))
+  if (node.getKind() == kind::BITVECTOR_BITOF
+      || node.getKind() == kind::CONST_BOOLEAN || hasBBAtom(node))
   {
     return;
   }