bv-to-int-module: implementations and stubs for translating operators (#7086)

This PR introduces most of the code for the translation of terms with operators. Some methods are left as stubs for future PRs.
A unit test is added with sanity checks for all implemented operators.

3 files changed, 579 insertions, 8 deletions

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index 02fdb4e05..5b9e0bfc4 100644
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -26,6 +26,7 @@
 #include "expr/skolem_manager.h"
 #include "options/option_exception.h"
 #include "options/uf_options.h"
+#include "theory/bv/theory_bv_utils.h"
 #include "theory/rewriter.h"
 #include "util/bitvector.h"
 #include "util/iand.h"
@@ -34,6 +35,13 @@
 namespace cvc5 {
 using namespace cvc5::theory;
 
+namespace {
+
+// A helper function to compute 2^b as a Rational
+Rational intpow2(uint64_t b) { return Rational(Integer(2).pow(b), Integer(1)); }
+
+}  // namespace
+
 IntBlaster::IntBlaster(context::Context* c,
                        options::SolveBVAsIntMode mode,
                        uint64_t granularity,
@@ -65,11 +73,24 @@ void IntBlaster::addBitwiseConstraint(Node bitwiseConstraint,
 
 Node IntBlaster::mkRangeConstraint(Node newVar, uint64_t k) { return Node(); }
 
-Node IntBlaster::maxInt(uint64_t k) { return Node(); }
+Node IntBlaster::maxInt(uint64_t k)
+{
+  Assert(k > 0);
+  Rational max_value = intpow2(k) - 1;
+  return d_nm->mkConst<Rational>(max_value);
+}
 
-Node IntBlaster::pow2(uint64_t k) { return Node(); }
+Node IntBlaster::pow2(uint64_t k)
+{
+  Assert(k >= 0);
+  return d_nm->mkConst<Rational>(intpow2(k));
+}
 
-Node IntBlaster::modpow2(Node n, uint64_t exponent) { return Node(); }
+Node IntBlaster::modpow2(Node n, uint64_t exponent)
+{
+  Node p2 = d_nm->mkConst<Rational>(intpow2(exponent));
+  return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2);
+}
 
 Node IntBlaster::makeBinary(Node n)
 {
@@ -194,8 +215,350 @@ Node IntBlaster::translateWithChildren(
     const std::vector<Node>& translated_children,
     std::vector<Node>& lemmas)
 {
-  Node binarized = makeBinary(original);
-  // continue to process the binarized version
+  // The translation of the original node is determined by the kind of
+  // the node.
+  kind::Kind_t oldKind = original.getKind();
+
+  // Some BV operators were eliminated before this point.
+  Assert(oldKind != kind::BITVECTOR_SDIV);
+  Assert(oldKind != kind::BITVECTOR_SREM);
+  Assert(oldKind != kind::BITVECTOR_SMOD);
+  Assert(oldKind != kind::BITVECTOR_XNOR);
+  Assert(oldKind != kind::BITVECTOR_NAND);
+  Assert(oldKind != kind::BITVECTOR_SUB);
+  Assert(oldKind != kind::BITVECTOR_REPEAT);
+  Assert(oldKind != kind::BITVECTOR_ROTATE_RIGHT);
+  Assert(oldKind != kind::BITVECTOR_ROTATE_LEFT);
+  Assert(oldKind != kind::BITVECTOR_COMP);
+  Assert(oldKind != kind::BITVECTOR_SGT);
+  Assert(oldKind != kind::BITVECTOR_SLE);
+  Assert(oldKind != kind::BITVECTOR_SGE);
+  Assert(oldKind != kind::EXISTS);
+
+  // BV division by zero was eliminated before this point.
+  Assert(oldKind != kind::BITVECTOR_UDIV
+         || !(original[1].isConst()
+              && original[1].getConst<BitVector>().getValue().isZero()));
+
+  // Store the translated node
+  Node returnNode;
+
+  // Translate according to the kind of the original node.
+  switch (oldKind)
+  {
+    case kind::BITVECTOR_ADD:
+    {
+      Assert(original.getNumChildren() == 2);
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      returnNode = createBVAddNode(
+          translated_children[0], translated_children[1], bvsize);
+      break;
+    }
+    case kind::BITVECTOR_MULT:
+    {
+      Assert(original.getNumChildren() == 2);
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      Node mult = d_nm->mkNode(kind::MULT, translated_children);
+      Node p2 = pow2(bvsize);
+      returnNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, mult, p2);
+      break;
+    }
+    case kind::BITVECTOR_UDIV:
+    {
+      // we use an ITE for the case where the second operand is 0.
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      Node pow2BvSize = pow2(bvsize);
+      Node divNode =
+          d_nm->mkNode(kind::INTS_DIVISION_TOTAL, translated_children);
+      returnNode = d_nm->mkNode(
+          kind::ITE,
+          d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero),
+          d_nm->mkNode(kind::MINUS, pow2BvSize, d_one),
+          divNode);
+      break;
+    }
+    case kind::BITVECTOR_UREM:
+    {
+      // we use an ITE for the case where the second operand is 0.
+      Node modNode =
+          d_nm->mkNode(kind::INTS_MODULUS_TOTAL, translated_children);
+      returnNode = d_nm->mkNode(
+          kind::ITE,
+          d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero),
+          translated_children[0],
+          modNode);
+      break;
+    }
+    case kind::BITVECTOR_NOT:
+    {
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      returnNode = createBVNotNode(translated_children[0], bvsize);
+      break;
+    }
+    case kind::BITVECTOR_NEG:
+    {
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      returnNode = createBVNegNode(translated_children[0], bvsize);
+      break;
+    }
+    case kind::BITVECTOR_TO_NAT:
+    {
+      // In this case, we already translated the child to integer.
+      // The result is simply the translated child.
+      returnNode = translated_children[0];
+      break;
+    }
+    case kind::INT_TO_BITVECTOR:
+    {
+      // In this case we take the original integer,
+      // modulo 2 to the power of the bit-width
+      returnNode =
+          modpow2(translated_children[0],
+                  original.getOperator().getConst<IntToBitVector>().d_size);
+      break;
+    }
+    case kind::BITVECTOR_OR:
+    {
+      Assert(translated_children.size() == 2);
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      returnNode = createBVOrNode(
+          translated_children[0], translated_children[1], bvsize, lemmas);
+      break;
+    }
+    case kind::BITVECTOR_XOR:
+    {
+      Assert(translated_children.size() == 2);
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      // Based on Hacker's Delight section 2-2 equation n:
+      // x xor y = x|y - x&y
+      Node bvor = createBVOrNode(
+          translated_children[0], translated_children[1], bvsize, lemmas);
+      Node bvand = createBVAndNode(
+          translated_children[0], translated_children[1], bvsize, lemmas);
+      returnNode = createBVSubNode(bvor, bvand, bvsize);
+      break;
+    }
+    case kind::BITVECTOR_AND:
+    {
+      Assert(translated_children.size() == 2);
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      returnNode = createBVAndNode(
+          translated_children[0], translated_children[1], bvsize, lemmas);
+      break;
+    }
+    case kind::BITVECTOR_SHL:
+    {
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      returnNode = createShiftNode(translated_children, bvsize, true);
+      break;
+    }
+    case kind::BITVECTOR_LSHR:
+    {
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      returnNode = createShiftNode(translated_children, bvsize, false);
+      break;
+    }
+    case kind::BITVECTOR_ASHR:
+    {
+      /*  From SMT-LIB2:
+       *  (bvashr s t) abbreviates
+       *     (ite (= ((_ extract |m-1| |m-1|) s) #b0)
+       *          (bvlshr s t)
+       *          (bvnot (bvlshr (bvnot s) t)))
+       *
+       *  Equivalently:
+       *  (bvashr s t) abbreviates
+       *      (ite (bvult s 100000...)
+       *           (bvlshr s t)
+       *           (bvnot (bvlshr (bvnot s) t)))
+       *
+       */
+      // signed_min is 100000...
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      Node signed_min = pow2(bvsize - 1);
+      Node condition =
+          d_nm->mkNode(kind::LT, translated_children[0], signed_min);
+      Node thenNode = createShiftNode(translated_children, bvsize, false);
+      std::vector<Node> children = {
+          createBVNotNode(translated_children[0], bvsize),
+          translated_children[1]};
+      Node elseNode =
+          createBVNotNode(createShiftNode(children, bvsize, false), bvsize);
+      returnNode = d_nm->mkNode(kind::ITE, condition, thenNode, elseNode);
+      break;
+    }
+    case kind::BITVECTOR_ITE:
+    {
+      // Lifted to a boolean ite.
+      Node cond = d_nm->mkNode(kind::EQUAL, translated_children[0], d_one);
+      returnNode = d_nm->mkNode(
+          kind::ITE, cond, translated_children[1], translated_children[2]);
+      break;
+    }
+    case kind::BITVECTOR_ZERO_EXTEND:
+    {
+      // zero extension does not change the integer translation.
+      returnNode = translated_children[0];
+      break;
+    }
+    case kind::BITVECTOR_SIGN_EXTEND:
+    {
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      returnNode =
+          createSignExtendNode(translated_children[0],
+                               bvsize,
+                               bv::utils::getSignExtendAmount(original));
+      break;
+    }
+    case kind::BITVECTOR_CONCAT:
+    {
+      // (concat a b) translates to a*2^k+b, k being the bitwidth of b.
+      uint64_t bvsizeRight = original[1].getType().getBitVectorSize();
+      Node pow2BvSizeRight = pow2(bvsizeRight);
+      Node a =
+          d_nm->mkNode(kind::MULT, translated_children[0], pow2BvSizeRight);
+      Node b = translated_children[1];
+      returnNode = d_nm->mkNode(kind::PLUS, a, b);
+      break;
+    }
+    case kind::BITVECTOR_EXTRACT:
+    {
+      // ((_ extract i j) a) is a / 2^j mod 2^{i-j+1}
+      // original = a[i:j]
+      uint64_t i = bv::utils::getExtractHigh(original);
+      uint64_t j = bv::utils::getExtractLow(original);
+      Assert(i >= j);
+      Node div = d_nm->mkNode(
+          kind::INTS_DIVISION_TOTAL, translated_children[0], pow2(j));
+      returnNode = modpow2(div, i - j + 1);
+      break;
+    }
+    case kind::EQUAL:
+    {
+      returnNode = d_nm->mkNode(kind::EQUAL, translated_children);
+      break;
+    }
+    case kind::BITVECTOR_ULT:
+    {
+      returnNode = d_nm->mkNode(kind::LT, translated_children);
+      break;
+    }
+    case kind::BITVECTOR_SLT:
+    {
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      returnNode = d_nm->mkNode(kind::LT,
+                                uts(translated_children[0], bvsize),
+                                uts(translated_children[1], bvsize));
+      break;
+    }
+    case kind::BITVECTOR_ULE:
+    {
+      returnNode = d_nm->mkNode(kind::LEQ, translated_children);
+      break;
+    }
+    case kind::BITVECTOR_UGT:
+    {
+      returnNode = d_nm->mkNode(kind::GT, translated_children);
+      break;
+    }
+    case kind::BITVECTOR_UGE:
+    {
+      returnNode = d_nm->mkNode(kind::GEQ, translated_children);
+      break;
+    }
+    case kind::BITVECTOR_ULTBV:
+    {
+      returnNode = d_nm->mkNode(kind::ITE,
+                                d_nm->mkNode(kind::LT, translated_children),
+                                d_one,
+                                d_zero);
+      break;
+    }
+    case kind::BITVECTOR_SLTBV:
+    {
+      uint64_t bvsize = original[0].getType().getBitVectorSize();
+      returnNode =
+          d_nm->mkNode(kind::ITE,
+                       d_nm->mkNode(kind::LT,
+                                    uts(translated_children[0], bvsize),
+                                    uts(translated_children[1], bvsize)),
+                       d_one,
+                       d_zero);
+      break;
+    }
+    case kind::ITE:
+    {
+      returnNode = d_nm->mkNode(oldKind, translated_children);
+      break;
+    }
+    case kind::APPLY_UF:
+    {
+      /**
+       * higher order logic allows comparing between functions
+       * The translation does not support this,
+       * as the translated functions may be different outside
+       * of the bounds that were relevant for the original
+       * bit-vectors.
+       */
+      if (childrenTypesChanged(original) && options::ufHo())
+      {
+        throw OptionException("bv-to-int does not support higher order logic ");
+      }
+      // Insert the translated application term to the cache
+      returnNode = d_nm->mkNode(kind::APPLY_UF, translated_children);
+      // Add range constraints if necessary.
+      // If the original range was a BV sort, the original application of
+      // the function must be within the range determined by the
+      // bitwidth.
+      if (original.getType().isBitVector())
+      {
+        addRangeConstraint(
+            returnNode, original.getType().getBitVectorSize(), lemmas);
+      }
+      break;
+    }
+    case kind::BOUND_VAR_LIST:
+    {
+      returnNode = d_nm->mkNode(oldKind, translated_children);
+      break;
+    }
+    case kind::FORALL:
+    {
+      returnNode = translateQuantifiedFormula(original);
+      break;
+    }
+    default:
+    {
+      // first, verify that we haven't missed
+      // any bv operator
+      Assert(theory::kindToTheoryId(oldKind) != THEORY_BV);
+
+      // In the default case, we have reached an operator that we do not
+      // translate directly to integers. The children whose types have
+      // changed from bv to int should be adjusted back to bv and then
+      // this term is reconstructed.
+      TypeNode resultingType;
+      if (original.getType().isBitVector())
+      {
+        resultingType = d_nm->integerType();
+      }
+      else
+      {
+        resultingType = original.getType();
+      }
+      Node reconstruction =
+          reconstructNode(original, resultingType, translated_children);
+      returnNode = reconstruction;
+      break;
+    }
+  }
+  Trace("int-blaster-debug") << "original: " << original << std::endl;
+  Trace("int-blaster-debug") << "returnNode: " << returnNode << std::endl;
+  return returnNode;
+}
+
+Node IntBlaster::createSignExtendNode(Node x, uint64_t bvsize, uint64_t amount)
+{
   return Node();
 }
 
@@ -419,4 +782,53 @@ Node IntBlaster::translateQuantifiedFormula(Node quantifiedNode)
   return Node();
 }
 
+Node IntBlaster::createBVAndNode(Node x,
+                                 Node y,
+                                 uint64_t bvsize,
+                                 std::vector<Node>& lemmas)
+{
+  return Node();
+}
+
+Node IntBlaster::createBVOrNode(Node x,
+                                Node y,
+                                uint64_t bvsize,
+                                std::vector<Node>& lemmas)
+{
+  // Based on Hacker's Delight section 2-2 equation h:
+  // x+y = x|y + x&y
+  // from which we deduce:
+  // x|y = x+y - x&y
+  Node plus = createBVAddNode(x, y, bvsize);
+  Node bvand = createBVAndNode(x, y, bvsize, lemmas);
+  return createBVSubNode(plus, bvand, bvsize);
+}
+
+Node IntBlaster::createBVSubNode(Node x, Node y, uint64_t bvsize)
+{
+  Node minus = d_nm->mkNode(kind::MINUS, x, y);
+  Node p2 = pow2(bvsize);
+  return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, minus, p2);
+}
+
+Node IntBlaster::createBVAddNode(Node x, Node y, uint64_t bvsize)
+{
+  Node plus = d_nm->mkNode(kind::PLUS, x, y);
+  Node p2 = pow2(bvsize);
+  return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, plus, p2);
+}
+
+Node IntBlaster::createBVNegNode(Node n, uint64_t bvsize)
+{
+  // Based on Hacker's Delight section 2-2 equation a:
+  // -x = ~x+1
+  Node p2 = pow2(bvsize);
+  return d_nm->mkNode(kind::MINUS, p2, n);
+}
+
+Node IntBlaster::createBVNotNode(Node n, uint64_t bvsize)
+{
+  return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n);
+}
+
 }  // namespace cvc5
diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h
index e98ae149e..1b4d5cdd6 100644
--- a/src/theory/bv/int_blaster.h
+++ b/src/theory/bv/int_blaster.h
@@ -74,6 +74,11 @@ namespace cvc5 {
 ** Tr(a=b) = Tr(a)=Tr(b)
 ** Tr((bvult a b)) = Tr(a) < Tr(b)
 ** Similar transformations are done for bvule, bvugt, and bvuge.
+** Tr((bvslt a b)) = Tr(uts(a)) < Tr(uts(b)),
+** where uts is a function that transforms unsigned
+** to signed representations. See more details
+** in the documentation of the function uts.
+** Similar transformations are done for the remaining comparators.
 **
 ** Bit-vector operators that are not listed above are either
 ** eliminated using the BV rewriter,
@@ -151,6 +156,35 @@ class IntBlaster
   /** Adds a constraint that encodes bitwise and */
   void addBitwiseConstraint(Node bitwiseConstraint, std::vector<Node>& lemmas);
 
+  /** Returns a node that represents the bitwise negation of n. */
+  Node createBVNotNode(Node n, uint64_t bvsize);
+
+  /** Returns a node that represents the arithmetic negation of n. */
+  Node createBVNegNode(Node n, uint64_t bvsize);
+
+  /** Returns a node that represents the bitwise and of x and y, based on the
+   * provided option. */
+  Node createBVAndNode(Node x,
+                       Node y,
+                       uint64_t bvsize,
+                       std::vector<Node>& lemmas);
+
+  /** Returns a node that represents the bitwise or of x and y, by translation
+   * to sum and bitwise and. */
+  Node createBVOrNode(Node x,
+                      Node y,
+                      uint64_t bvsize,
+                      std::vector<Node>& lemmas);
+
+  /** Returns a node that represents the sum of x and y. */
+  Node createBVAddNode(Node x, Node y, uint64_t bvsize);
+
+  /** Returns a node that represents the difference of x and y. */
+  Node createBVSubNode(Node x, Node y, uint64_t bvsize);
+
+  /** Returns a node that represents the signed extension of x by amount. */
+  Node createSignExtendNode(Node x, uint64_t bvsize, uint64_t amount);
+
   /**
    * Whenever we introduce an integer variable that represents a bit-vector
    * variable, we need to guard the range of the newly introduced variable.
diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp
index b17ccf342..f76305db6 100644
--- a/test/unit/theory/theory_bv_int_blaster_white.cpp
+++ b/test/unit/theory/theory_bv_int_blaster_white.cpp
@@ -21,6 +21,7 @@
 #include "options/options.h"
 #include "test_smt.h"
 #include "theory/bv/int_blaster.h"
+#include "theory/bv/theory_bv_utils.h"
 #include "util/bitvector.h"
 #include "util/rational.h"
 namespace cvc5 {
@@ -45,7 +46,7 @@ class TestTheoryWhiteBvIntblaster : public TestSmtNoFinishInit
   Node d_one;
 };
 
-TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_constants)
+TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants)
 {
   // place holders for lemmas and skolem
   std::vector<Node> lemmas;
@@ -67,7 +68,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_constants)
   ASSERT_EQ(seven, result);
 }
 
-TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_symbolic_constant)
+TEST_F(TestTheoryWhiteBvIntblaster, intblaster_symbolic_constant)
 {
   // place holders for lemmas and skolem
   std::vector<Node> lemmas;
@@ -88,7 +89,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_symbolic_constant)
   ASSERT_EQ(resultSquared, result);
 }
 
-TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_uf)
+TEST_F(TestTheoryWhiteBvIntblaster, intblaster_uf)
 {
   // place holders for lemmas and skolem
   std::vector<Node> lemmas;
@@ -119,5 +120,129 @@ TEST_F(TestTheoryWhiteBvIntblaster, bitblaster_uf)
   ASSERT_TRUE(resultRange.isBoolean());
 }
 
+/** Check all cases of the translation.
+ * This is a sanity check, that noly verifies
+ * the expected type, and that there were no
+ * failures.
+ */
+TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children)
+{
+  // place holders for lemmas and skolem
+  std::vector<Node> lemmas;
+  std::map<Node, Node> skolems;
+  IntBlaster intBlaster(
+      d_smtEngine->getContext(), options::SolveBVAsIntMode::SUM, 1, true);
+
+  // bit-vector variables
+  TypeNode bvType = d_nodeManager->mkBitVectorType(4);
+  Node v1 = d_nodeManager->mkVar("v1", bvType);
+  Node v2 = d_nodeManager->mkVar("v2", bvType);
+
+  // translated integer variables
+  Node i1 = intBlaster.translateNoChildren(v1, lemmas, skolems);
+  Node i2 = intBlaster.translateNoChildren(v2, lemmas, skolems);
+
+  // if original is BV, result should be Int.
+  // Otherwise, they should have the same type.
+  Node original;
+  Node result;
+
+  // sum
+  original = d_nodeManager->mkNode(BITVECTOR_ADD, v1, v2);
+  result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+  ASSERT_TRUE(result.getType().isInteger());
+
+  // multiplication
+  original = d_nodeManager->mkNode(BITVECTOR_MULT, v1, v2);
+  result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+  ASSERT_TRUE(result.getType().isInteger());
+
+  // division 1
+  original = d_nodeManager->mkNode(BITVECTOR_UDIV, v1, v2);
+  result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+  ASSERT_TRUE(result.getType().isInteger());
+
+  // division 2
+  original = d_nodeManager->mkNode(BITVECTOR_UREM, v1, v2);
+  result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+  ASSERT_TRUE(result.getType().isInteger());
+
+  // bit-wise negation
+  original = d_nodeManager->mkNode(BITVECTOR_NOT, v1);
+  result = intBlaster.translateWithChildren(original, {i1}, lemmas);
+  ASSERT_TRUE(result.getType().isInteger());
+
+  // arithmetic negation
+  original = d_nodeManager->mkNode(BITVECTOR_NEG, v1);
+  result = intBlaster.translateWithChildren(original, {i1}, lemmas);
+  ASSERT_TRUE(result.getType().isInteger());
+
+  // bv2nat
+  original = d_nodeManager->mkNode(BITVECTOR_TO_NAT, v1);
+  result = intBlaster.translateWithChildren(original, {i1}, lemmas);
+  ASSERT_TRUE(result.getType().isInteger());
+
+  // int2bv
+  Node intToBVOp = d_nodeManager->mkConst<IntToBitVector>(IntToBitVector(4));
+  original = d_nodeManager->mkNode(intToBVOp, i1);
+  result = intBlaster.translateWithChildren(original, {i1}, lemmas);
+  ASSERT_TRUE(result.getType().isInteger());
+
+  // zero extend
+  Node zeroExtOp =
+      d_nodeManager->mkConst<BitVectorZeroExtend>(BitVectorZeroExtend(4));
+  original = d_nodeManager->mkNode(zeroExtOp, v1);
+  result = intBlaster.translateWithChildren(original, {i1}, lemmas);
+  ASSERT_TRUE(result.getType().isInteger());
+
+  // extract + BV ITE
+  Node extract = theory::bv::utils::mkExtract(v1, 0, 0);
+  original = d_nodeManager->mkNode(BITVECTOR_ITE, extract, v2, v1);
+  Node intExtract = intBlaster.translateWithChildren(extract, {i1}, lemmas);
+  result =
+      intBlaster.translateWithChildren(original, {intExtract, i1, i2}, lemmas);
+  ASSERT_TRUE(result.getType().isInteger());
+  ASSERT_TRUE(intExtract.getType().isInteger());
+
+  // concat
+  original = d_nodeManager->mkNode(BITVECTOR_CONCAT, v1, v2);
+  result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+  ASSERT_TRUE(result.getType().isInteger());
+
+  // predicates
+  original = d_nodeManager->mkNode(EQUAL, v1, v2);
+  result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+  ASSERT_TRUE(result.getType().isBoolean());
+
+  original = d_nodeManager->mkNode(BITVECTOR_ULT, v1, v2);
+  result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+  ASSERT_TRUE(result.getType().isBoolean());
+
+  original = d_nodeManager->mkNode(BITVECTOR_ULE, v1, v2);
+  result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+  ASSERT_TRUE(result.getType().isBoolean());
+
+  original = d_nodeManager->mkNode(BITVECTOR_UGT, v1, v2);
+  result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+  ASSERT_TRUE(result.getType().isBoolean());
+
+  original = d_nodeManager->mkNode(BITVECTOR_UGE, v1, v2);
+  result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+  ASSERT_TRUE(result.getType().isBoolean());
+
+  // BVULT with a BV result
+  original = d_nodeManager->mkNode(BITVECTOR_ULTBV, v1, v2);
+  result = intBlaster.translateWithChildren(original, {i1, i2}, lemmas);
+  ASSERT_TRUE(result.getType().isInteger());
+
+  // function application
+  TypeNode funType = d_nodeManager->mkFunctionType({bvType}, bvType);
+  Node f = d_nodeManager->mkVar("f", funType);
+  Node g = intBlaster.translateNoChildren(f, lemmas, skolems);
+  original = d_nodeManager->mkNode(APPLY_UF, f, v1);
+  result = intBlaster.translateWithChildren(original, {g, i1}, lemmas);
+  ASSERT_TRUE(result.getType().isInteger());
+}
+
 }  // namespace test
 }  // namespace cvc5