Do not print BITVECTOR_EAGER_ATOM in cpc proofs (cvc5#11377)

BV_EAGER_ATOM can now be `refl`.

Note that I've opened a wishue if we want a deeper refactoring to never
print this kind at all, which will require changes to the smt2 printer.

proofs/eo/cpc/theories/BitVectors.eo

@@ -343,8 +343,6 @@
   (BitVec m) Int)
 )
 
-(declare-const BITVECTOR_EAGER_ATOM (-> Bool Bool))
-
 ; internal operators
 
 (declare-const @bit

src/proof/alf/alf_node_converter.cpp

@@ -295,6 +295,13 @@ Node AlfNodeConverter::postConvert(Node n)
       return mkInternalApp("to_fp_bv", children, tn);
     }
   }
+  else if (k == Kind::BITVECTOR_EAGER_ATOM)
+  {
+    // For now, we explicity remove the application.
+    // https://github.com/cvc5/cvc5-wishues/issues/156: if the smt2 printer
+    // is refactored to silently ignore this kind, this case can be deleted.
+    return n[0];
+  }
   else if (GenericOp::isIndexedOperatorKind(k))
   {
     TypeNode tn = n.getType();

src/proof/alf/alf_printer.cpp

@@ -180,6 +180,7 @@ bool AlfPrinter::isHandled(const Options& opts, const ProofNode* pfn)
     case ProofRule::QUANT_VAR_REORDERING:
     case ProofRule::ENCODE_EQ_INTRO:
     case ProofRule::HO_APP_ENCODE:
+    case ProofRule::BV_EAGER_ATOM:
     case ProofRule::ACI_NORM:
     case ProofRule::ARITH_POLY_NORM:
     case ProofRule::ARITH_POLY_NORM_REL:
@@ -496,7 +497,8 @@ std::string AlfPrinter::getRuleName(const ProofNode* pfn) const
     ss << id;
     return ss.str();
   }
-  else if (r == ProofRule::ENCODE_EQ_INTRO || r == ProofRule::HO_APP_ENCODE)
+  else if (r == ProofRule::ENCODE_EQ_INTRO || r == ProofRule::HO_APP_ENCODE
+           || r == ProofRule::BV_EAGER_ATOM)
   {
     // ENCODE_EQ_INTRO proves (= t (convert t)) from argument t,
     // where (convert t) is indistinguishable from t according to the proof.