1 files changed, 3 insertions, 48 deletions
diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index c1cf0338a..d20c3ecc0 100644
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -730,63 +730,18 @@ enum class PfRule : uint32_t
   // ---------------------
   // Conclusion: (= t bitblast(t))
   BV_BITBLAST,
-  // ======== Bitblast Bit-Vector Constant
+  // ======== Bitblast Bit-Vector Constant, Variable
   // Children: none
   // Arguments: (= t bitblast(t))
   // ---------------------
   // Conclusion: (= t bitblast(t))
-  BV_BITBLAST_CONST,
-  // ======== Bitblast Bit-Vector Variable
-  // Children: none
-  // Arguments: (= t bitblast(t))
-  // ---------------------
-  // Conclusion: (= t bitblast(t))
-  BV_BITBLAST_VAR,
   // ======== Bitblast Bit-Vector Terms
-  // TODO cvc4-projects issue #275
   // Children: none
   // Arguments: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t))
   // ---------------------
   // Conclusion: (= (KIND bitblast(child_1) ... bitblast(child_n)) bitblast(t))
-  BV_BITBLAST_EQUAL,
-  BV_BITBLAST_ULT,
-  BV_BITBLAST_ULE,
-  BV_BITBLAST_UGT,
-  BV_BITBLAST_UGE,
-  BV_BITBLAST_SLT,
-  BV_BITBLAST_SLE,
-  BV_BITBLAST_SGT,
-  BV_BITBLAST_SGE,
-  BV_BITBLAST_NOT,
-  BV_BITBLAST_CONCAT,
-  BV_BITBLAST_AND,
-  BV_BITBLAST_OR,
-  BV_BITBLAST_XOR,
-  BV_BITBLAST_XNOR,
-  BV_BITBLAST_NAND,
-  BV_BITBLAST_NOR,
-  BV_BITBLAST_COMP,
-  BV_BITBLAST_MULT,
-  BV_BITBLAST_ADD,
-  BV_BITBLAST_SUB,
-  BV_BITBLAST_NEG,
-  BV_BITBLAST_UDIV,
-  BV_BITBLAST_UREM,
-  BV_BITBLAST_SDIV,
-  BV_BITBLAST_SREM,
-  BV_BITBLAST_SMOD,
-  BV_BITBLAST_SHL,
-  BV_BITBLAST_LSHR,
-  BV_BITBLAST_ASHR,
-  BV_BITBLAST_ULTBV,
-  BV_BITBLAST_SLTBV,
-  BV_BITBLAST_ITE,
-  BV_BITBLAST_EXTRACT,
-  BV_BITBLAST_REPEAT,
-  BV_BITBLAST_ZERO_EXTEND,
-  BV_BITBLAST_SIGN_EXTEND,
-  BV_BITBLAST_ROTATE_RIGHT,
-  BV_BITBLAST_ROTATE_LEFT,
+  BV_BITBLAST_STEP,
+
   // ======== Eager Atom
   // Children: none
   // Arguments: (F)