From c971f498611314c4f6ba32fda224e922a73165ec Mon Sep 17 00:00:00 2001
From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Fri, 19 Apr 2024 22:18:19 -0300
Subject: [PATCH] use old bbt/bitof

---
 src/proof/alethe/alethe_node_converter.cpp | 26 ++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/src/proof/alethe/alethe_node_converter.cpp b/src/proof/alethe/alethe_node_converter.cpp
index 85c597b667a..e9b06dc8000 100644
--- a/src/proof/alethe/alethe_node_converter.cpp
+++ b/src/proof/alethe/alethe_node_converter.cpp
@@ -18,6 +18,7 @@
 #include "expr/node_algorithm.h"
 #include "expr/skolem_manager.h"
 #include "proof/proof_rule_checker.h"
+#include "util/bitvector.h"
 #include "util/rational.h"
 
 namespace cvc5::internal {
@@ -41,6 +42,31 @@ Node AletheNodeConverter::postConvert(Node n)
   Kind k = n.getKind();
   switch (k)
   {
+    case Kind::BITVECTOR_BITOF:
+    {
+      std::stringstream ss;
+      ss << "(_ bitOf " << n.getOperator().getConst<BitVectorBitOf>().d_bitIndex
+         << ")";
+      TypeNode fType = nm->mkFunctionType(n[0].getType(), n.getType());
+      Node op = mkInternalSymbol(ss.str(), fType, true);
+      Node converted = nm->mkNode(Kind::APPLY_UF, op, n[0]);
+      return converted;
+    }
+    case Kind::BITVECTOR_BB_TERM:
+    {
+      std::vector<Node> children;
+      std::vector<TypeNode> childrenTypes;
+      for (const Node& c : n)
+      {
+        childrenTypes.push_back(c.getType());
+        children.push_back(c);
+      }
+      TypeNode fType = nm->mkFunctionType(childrenTypes, n.getType());
+      Node op = mkInternalSymbol("bbT", fType, true);
+      children.insert(children.begin(), op);
+      Node converted = nm->mkNode(Kind::APPLY_UF, children);
+      return converted;
+    }
     case Kind::BITVECTOR_EAGER_ATOM:
     {
       std::stringstream ss;