Integrate new int-blaster (#7781)

This PR removes the code that translates from bit-vectors to integers from the bv_to_int preprocessing pass, and replaces it with a call to the IntBlaster module.

Tests are updated and added, as well as other minor changes.

Solves the following issues (and contains corresponding tests):
cvc5/cvc5-projects#345
cvc5/cvc5-projects#344
cvc5/cvc5-projects#343

@mpreiner FYI

35 files changed, 210 insertions, 1398 deletions

diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
index f106f1ccf..ac1edeb96 100644
--- a/src/preprocessing/passes/bv_to_int.cpp
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -19,1060 +19,90 @@
 #include "preprocessing/passes/bv_to_int.h"
 
 #include <cmath>
-#include <sstream>
 #include <string>
 #include <unordered_map>
 #include <vector>
 
 #include "expr/node.h"
 #include "expr/node_traversal.h"
-#include "expr/skolem_manager.h"
-#include "options/option_exception.h"
 #include "options/smt_options.h"
 #include "options/uf_options.h"
-#include "preprocessing/assertion_pipeline.h"
-#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
+#include "preprocessing/assertion_pipeline.h"
 #include "theory/bv/theory_bv_rewrite_rules_simplification.h"
 #include "theory/rewriter.h"
-#include "util/bitvector.h"
-#include "util/iand.h"
-#include "util/rational.h"
 
 namespace cvc5 {
 namespace preprocessing {
 namespace passes {
 
 using namespace std;
-using namespace cvc5::kind;
 using namespace cvc5::theory;
 using namespace cvc5::theory::bv;
 
-namespace {
-
-Rational intpow2(uint64_t b)
-{
-  return Rational(Integer(2).pow(b), Integer(1));
-}
-
-} //end empty namespace
-
-Node BVToInt::mkRangeConstraint(Node newVar, uint64_t k)
-{
-  Node lower = d_nm->mkNode(kind::LEQ, d_zero, newVar);
-  Node upper = d_nm->mkNode(kind::LT, newVar, pow2(k));
-  Node result = d_nm->mkNode(kind::AND, lower, upper);
-  return rewrite(result);
-}
-
-Node BVToInt::maxInt(uint64_t k)
-{
-  Assert(k > 0);
-  Rational max_value = intpow2(k) - 1;
-  return d_nm->mkConst(CONST_RATIONAL, max_value);
-}
-
-Node BVToInt::pow2(uint64_t k)
-{
-  Assert(k >= 0);
-  return d_nm->mkConst(CONST_RATIONAL, Rational(intpow2(k)));
-}
-
-Node BVToInt::modpow2(Node n, uint64_t exponent)
-{
-  Node p2 = d_nm->mkConst(CONST_RATIONAL, Rational(intpow2(exponent)));
-  return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2);
-}
-
-/**
- * Binarizing n via post-order traversal.
- */
-Node BVToInt::makeBinary(Node n)
-{
-  for (TNode current : NodeDfsIterable(n,
-                                       VisitOrder::POSTORDER,
-                                       // skip visited nodes
-                                       [this](TNode tn) {
-                                         return d_binarizeCache.find(tn)
-                                                != d_binarizeCache.end();
-                                       }))
-  {
-    uint64_t numChildren = current.getNumChildren();
-    /*
-     * We already visited the sub-dag rooted at the current node,
-     * and binarized all its children.
-     * Now we binarize the current node itself.
-     */
-    kind::Kind_t k = current.getKind();
-    if ((numChildren > 2)
-        && (k == kind::BITVECTOR_ADD || k == kind::BITVECTOR_MULT
-            || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR
-            || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT))
-    {
-      // We only binarize bvadd, bvmul, bvand, bvor, bvxor, bvconcat
-      Assert(d_binarizeCache.find(current[0]) != d_binarizeCache.end());
-      Node result = d_binarizeCache[current[0]];
-      for (uint64_t i = 1; i < numChildren; i++)
-      {
-        Assert(d_binarizeCache.find(current[i]) != d_binarizeCache.end());
-        Node child = d_binarizeCache[current[i]];
-        result = d_nm->mkNode(current.getKind(), result, child);
-      }
-      d_binarizeCache[current] = result;
-    }
-    else if (numChildren > 0)
-    {
-      // current has children, but we do not binarize it
-      NodeBuilder builder(k);
-      if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
-      {
-        builder << current.getOperator();
-      }
-      for (Node child : current)
-      {
-        builder << d_binarizeCache[child].get();
-      }
-      d_binarizeCache[current] = builder.constructNode();
-    }
-    else
-    {
-      // current has no children
-      d_binarizeCache[current] = current;
-    }
-  }
-  return d_binarizeCache[n];
-}
-
-/**
- * We traverse n and perform rewrites both on the way down and on the way up.
- * On the way down we rewrite the node but not it's children.
- * On the way up, we update the node's children to the rewritten ones.
- * For each sub-node, we perform rewrites to eliminate operators.
- * Then, the original children are added to toVisit stack so that we rewrite
- * them as well.
- */
-Node BVToInt::eliminationPass(Node n)
-{
-  std::vector<Node> toVisit;
-  toVisit.push_back(n);
-  Node current;
-  while (!toVisit.empty())
-  {
-    current = toVisit.back();
-    // assert that the node is binarized
-    // The following variable is only used in assertions
-    CVC5_UNUSED kind::Kind_t k = current.getKind();
-    uint64_t numChildren = current.getNumChildren();
-    Assert((numChildren == 2)
-           || !(k == kind::BITVECTOR_ADD || k == kind::BITVECTOR_MULT
-                || k == kind::BITVECTOR_AND || k == kind::BITVECTOR_OR
-                || k == kind::BITVECTOR_XOR || k == kind::BITVECTOR_CONCAT));
-    toVisit.pop_back();
-    bool inEliminationCache =
-        (d_eliminationCache.find(current) != d_eliminationCache.end());
-    bool inRebuildCache =
-        (d_rebuildCache.find(current) != d_rebuildCache.end());
-    if (!inEliminationCache)
-    {
-      // current is not the elimination of any previously-visited node
-      // current hasn't been eliminated yet.
-      // eliminate operators from it using rewrite rules
-      Node currentEliminated =
-          FixpointRewriteStrategy<RewriteRule<UdivZero>,
-                                  RewriteRule<SdivEliminateFewerBitwiseOps>,
-                                  RewriteRule<SremEliminateFewerBitwiseOps>,
-                                  RewriteRule<SmodEliminateFewerBitwiseOps>,
-                                  RewriteRule<XnorEliminate>,
-                                  RewriteRule<NandEliminate>,
-                                  RewriteRule<NorEliminate>,
-                                  RewriteRule<NegEliminate>,
-                                  RewriteRule<XorEliminate>,
-                                  RewriteRule<OrEliminate>,
-                                  RewriteRule<SubEliminate>,
-                                  RewriteRule<RepeatEliminate>,
-                                  RewriteRule<RotateRightEliminate>,
-                                  RewriteRule<RotateLeftEliminate>,
-                                  RewriteRule<CompEliminate>,
-                                  RewriteRule<SleEliminate>,
-                                  RewriteRule<SltEliminate>,
-                                  RewriteRule<SgtEliminate>,
-                                  RewriteRule<SgeEliminate>>::apply(current);
-
-      // save in the cache
-      d_eliminationCache[current] = currentEliminated;
-      // also assign the eliminated now to itself to avoid revisiting.
-      d_eliminationCache[currentEliminated] = currentEliminated;
-      // put the eliminated node in the rebuild cache, but mark that it hasn't
-      // yet been rebuilt by assigning null.
-      d_rebuildCache[currentEliminated] = Node();
-      // Push the eliminated node to the stack
-      toVisit.push_back(currentEliminated);
-      // Add the children to the stack for future processing.
-      toVisit.insert(
-          toVisit.end(), currentEliminated.begin(), currentEliminated.end());
-    }
-    if (inRebuildCache)
-    {
-      // current was already added to the rebuild cache.
-      if (d_rebuildCache[current].get().isNull())
-      {
-        // current wasn't rebuilt yet.
-        numChildren = current.getNumChildren();
-        if (numChildren == 0)
-        {
-          // We only eliminate operators that are not nullary.
-          d_rebuildCache[current] = current;
-        }
-        else
-        {
-          // The main operator is replaced, and the children
-          // are replaced with their eliminated counterparts.
-          NodeBuilder builder(current.getKind());
-          if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
-          {
-            builder << current.getOperator();
-          }
-          for (Node child : current)
-          {
-            Assert(d_eliminationCache.find(child) != d_eliminationCache.end());
-            Node eliminatedChild = d_eliminationCache[child];
-            Assert(d_rebuildCache.find(eliminatedChild) != d_eliminationCache.end());
-            Assert(!d_rebuildCache[eliminatedChild].get().isNull());
-            builder << d_rebuildCache[eliminatedChild].get();
-          }
-          d_rebuildCache[current] = builder.constructNode();
-        }
-      }
-    }
-  }
-  Assert(d_eliminationCache.find(n) != d_eliminationCache.end());
-  Node eliminated = d_eliminationCache[n];
-  Assert(d_rebuildCache.find(eliminated) != d_rebuildCache.end());
-  Assert(!d_rebuildCache[eliminated].get().isNull());
-  return d_rebuildCache[eliminated];
-}
-
-/**
- * Translate n to Integers via post-order traversal.
- */
-Node BVToInt::bvToInt(Node n)
-{
-  // make sure the node is re-written before processing it.
-  n = rewrite(n);
-  n = makeBinary(n);
-  n = eliminationPass(n);
-  // binarize again, in case the elimination pass introduced
-  // non-binary terms (as can happen by RepeatEliminate, for example).
-  n = makeBinary(n);
-  vector<Node> toVisit;
-  toVisit.push_back(n);
-
-  while (!toVisit.empty())
-  {
-    Node current = toVisit.back();
-    uint64_t currentNumChildren = current.getNumChildren();
-    if (d_bvToIntCache.find(current) == d_bvToIntCache.end())
-    {
-      // This is the first time we visit this node and it is not in the cache.
-      // We mark this node as visited but not translated by assiging
-      // a null node to it.
-      d_bvToIntCache[current] = Node();
-      // all the node's children are added to the stack to be visited
-      // before visiting this node again.
-      toVisit.insert(toVisit.end(), current.begin(), current.end());
-      // If this is a UF applicatinon, we also add the function to
-      // toVisit.
-      if (current.getKind() == kind::APPLY_UF)
-      {
-        toVisit.push_back(current.getOperator());
-      }
-    }
-    else
-    {
-      // We already visited and translated this node
-      if (!d_bvToIntCache[current].get().isNull())
-      {
-        // We are done computing the translation for current
-        toVisit.pop_back();
-      }
-      else
-      {
-        // We are now visiting current on the way back up.
-        // This is when we do the actual translation.
-        Node translation;
-        if (currentNumChildren == 0)
-        {
-          translation = translateNoChildren(current);
-        }
-        else
-        {
-          /**
-           * The current node has children.
-           * Since we are on the way back up,
-           * these children were already translated.
-           * We save their translation for easy access.
-           * If the node's kind is APPLY_UF,
-           * we also need to include the translated uninterpreted function in
-           * this list.
-           */
-          vector<Node> translated_children;
-          if (current.getKind() == kind::APPLY_UF)
-          {
-            translated_children.push_back(
-                d_bvToIntCache[current.getOperator()]);
-          }
-          for (uint64_t i = 0; i < currentNumChildren; i++)
-          {
-            translated_children.push_back(d_bvToIntCache[current[i]]);
-          }
-          translation = translateWithChildren(current, translated_children);
-        }
-        // Map the current node to its translation in the cache.
-        d_bvToIntCache[current] = translation;
-        // Also map the translation to itself.
-        d_bvToIntCache[translation] = translation;
-        toVisit.pop_back();
-      }
-    }
-  }
-  return d_bvToIntCache[n].get();
-}
-
-Node BVToInt::translateWithChildren(Node original,
-                                    const vector<Node>& translated_children)
-{
-  // The translation of the original node is determined by the kind of
-  // the node.
-  kind::Kind_t oldKind = original.getKind();
-  // ultbv and sltbv were supposed to be eliminated before this point.
-  Assert(oldKind != kind::BITVECTOR_ULTBV);
-  Assert(oldKind != kind::BITVECTOR_SLTBV);
-  // The following variable will only be used in assertions.
-  CVC5_UNUSED uint64_t originalNumChildren = original.getNumChildren();
-  Node returnNode;
-  switch (oldKind)
-  {
-    case kind::BITVECTOR_ADD:
-    {
-      Assert(originalNumChildren == 2);
-      uint64_t bvsize = original[0].getType().getBitVectorSize();
-      Node plus = d_nm->mkNode(kind::PLUS, translated_children);
-      Node p2 = pow2(bvsize);
-      returnNode = d_nm->mkNode(kind::INTS_MODULUS_TOTAL, plus, p2);
-      break;
-    }
-    case kind::BITVECTOR_MULT:
-    {
-      Assert(originalNumChildren == 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:
-    {
-      uint64_t bvsize = original[0].getType().getBitVectorSize();
-      // we use an ITE for the case where the second operand is 0.
-      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();
-      // we use a specified function to generate the node.
-      returnNode = createBVNotNode(translated_children[0], bvsize);
-      break;
-    }
-    case kind::BITVECTOR_TO_NAT:
-    {
-      // In this case, we already translated the child to integer.
-      // So the result is the translated child.
-      returnNode = translated_children[0];
-      break;
-    }
-    case kind::INT_TO_BITVECTOR:
-    {
-      // ((_ int2bv n) t) ---> (mod t 2^n)
-      size_t sz = original.getOperator().getConst<IntToBitVector>().d_size;
-      returnNode = d_nm->mkNode(
-          kind::INTS_MODULUS_TOTAL, translated_children[0], pow2(sz));
-    }
-    break;
-    case kind::BITVECTOR_AND:
-    {
-      // We support three configurations:
-      // 1. translating to IAND
-      // 2. translating back to BV (using BITVECTOR_TO_NAT and INT_TO_BV
-      // operators)
-      // 3. translating into a sum
-      uint64_t bvsize = original[0].getType().getBitVectorSize();
-      if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::IAND)
-      {
-        Node iAndOp = d_nm->mkConst(IntAnd(bvsize));
-        returnNode = d_nm->mkNode(
-            kind::IAND, iAndOp, translated_children[0], translated_children[1]);
-      }
-      else if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::BV)
-      {
-        // translate the children back to BV
-        Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize));
-        Node x = translated_children[0];
-        Node y = translated_children[1];
-        Node bvx = d_nm->mkNode(intToBVOp, x);
-        Node bvy = d_nm->mkNode(intToBVOp, y);
-        // perform bvand on the bit-vectors
-        Node bvand = d_nm->mkNode(kind::BITVECTOR_AND, bvx, bvy);
-        // translate the result to integers
-        returnNode = d_nm->mkNode(kind::BITVECTOR_TO_NAT, bvand);
-      }
-      else
-      {
-        Assert(options().smt.solveBVAsInt == options::SolveBVAsIntMode::SUM);
-        // Construct a sum of ites, based on granularity.
-        Assert(translated_children.size() == 2);
-        returnNode =
-            d_iandUtils.createSumNode(translated_children[0],
-                                      translated_children[1],
-                                      bvsize,
-                                      options().smt.BVAndIntegerGranularity);
-      }
-      break;
-    }
-    case kind::BITVECTOR_SHL:
-    {
-      /**
-       * a << b is a*2^b.
-       * The exponentiation is simulated by an ite.
-       * Only cases where b <= bit width are considered.
-       * Otherwise, the result is 0.
-       */
-      uint64_t bvsize = original[0].getType().getBitVectorSize();
-      returnNode = createShiftNode(translated_children, bvsize, true);
-      break;
-    }
-    case kind::BITVECTOR_LSHR:
-    {
-      /**
-       * a >> b is a div 2^b.
-       * The exponentiation is simulated by an ite.
-       * Only cases where b <= bit width are considered.
-       * Otherwise, the result is 0.
-       */
-      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)))
-       *
-       */
-      uint64_t bvsize = original[0].getType().getBitVectorSize();
-      // signed_min is 100000...
-      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);
-      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:
-    {
-      returnNode = translated_children[0];
-      break;
-    }
-    case kind::BITVECTOR_SIGN_EXTEND:
-    {
-      uint64_t bvsize = original[0].getType().getBitVectorSize();
-      Node arg = translated_children[0];
-      if (arg.isConst())
-      {
-        Rational c(arg.getConst<Rational>());
-        Rational twoToKMinusOne(intpow2(bvsize - 1));
-        uint64_t amount = bv::utils::getSignExtendAmount(original);
-        /* if the msb is 0, this is like zero_extend.
-         *  msb is 0 <-> the value is less than 2^{bvsize-1}
-         */
-        if (c < twoToKMinusOne || amount == 0)
-        {
-          returnNode = arg;
-        }
-        else
-        {
-          /* otherwise, we add the integer equivalent of
-           * 11....1 `amount` times
-           */
-          Rational max_of_amount = intpow2(amount) - 1;
-          Rational mul = max_of_amount * intpow2(bvsize);
-          Rational sum = mul + c;
-          returnNode = d_nm->mkConst(CONST_RATIONAL, sum);
-        }
-      }
-      else
-      {
-        uint64_t amount = bv::utils::getSignExtendAmount(original);
-        if (amount == 0)
-        {
-          returnNode = translated_children[0];
-        }
-        else
-        {
-          Rational twoToKMinusOne(intpow2(bvsize - 1));
-          Node minSigned = d_nm->mkConst(CONST_RATIONAL, twoToKMinusOne);
-          /* condition checks whether the msb is 1.
-           * This holds when the integer value is smaller than
-           * 100...0, which is 2^{bvsize-1}.
-           */
-          Node condition = d_nm->mkNode(kind::LT, arg, minSigned);
-          Node thenResult = arg;
-          Node left = maxInt(amount);
-          Node mul = d_nm->mkNode(kind::MULT, left, pow2(bvsize));
-          Node sum = d_nm->mkNode(kind::PLUS, mul, arg);
-          Node elseResult = sum;
-          Node ite = d_nm->mkNode(kind::ITE, condition, thenResult, elseResult);
-          returnNode = ite;
-        }
-      }
-      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_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::LT:
-    {
-      returnNode = d_nm->mkNode(kind::LT, translated_children);
-      break;
-    }
-    case kind::LEQ:
-    {
-      returnNode = d_nm->mkNode(kind::LEQ, translated_children);
-      break;
-    }
-    case kind::GT:
-    {
-      returnNode = d_nm->mkNode(kind::GT, translated_children);
-      break;
-    }
-    case kind::GEQ:
-    {
-      returnNode = d_nm->mkNode(kind::GEQ, translated_children);
-      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) && logicInfo().isHigherOrder())
-      {
-        throw TypeCheckingExceptionPrivate(
-            original,
-            string("Cannot translate to Int: ") + original.toString());
-      }
-      // 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())
-      {
-        d_rangeAssertions.insert(mkRangeConstraint(
-            returnNode, original.getType().getBitVectorSize()));
-      }
-      break;
-    }
-    case kind::BOUND_VAR_LIST:
-    {
-      returnNode = d_nm->mkNode(oldKind, translated_children);
-      break;
-    }
-    case kind::FORALL:
-    {
-      returnNode = translateQuantifiedFormula(original);
-      break;
-    }
-    default:
-    {
-      Assert(oldKind != kind::EXISTS);  // Exists is eliminated by the rewriter.
-      // 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("bv-to-int-debug") << "original: " << original << endl;
-  Trace("bv-to-int-debug") << "returnNode: " << returnNode << endl;
-  return returnNode;
-}
-
-Node BVToInt::translateNoChildren(Node original)
-{
-  SkolemManager* sm = d_nm->getSkolemManager();
-  Node translation;
-  Assert(original.isVar() || original.isConst());
-  if (original.isVar())
-  {
-    if (original.getType().isBitVector())
-    {
-      // For bit-vector variables, we create fresh integer variables.
-      if (original.getKind() == kind::BOUND_VARIABLE)
-      {
-        // Range constraints for the bound integer variables are not added now.
-        // they will be added once the quantifier itself is handled.
-        std::stringstream ss;
-        ss << original;
-        translation = d_nm->mkBoundVar(ss.str() + "_int", d_nm->integerType());
-      }
-      else
-      {
-        // New integer variables  that are not bound (symbolic constants)
-        // are added together with range constraints induced by the 
-        // bit-width of the original bit-vector variables.
-        Node newVar = sm->mkDummySkolem("__bvToInt_var",
-                                        d_nm->integerType(),
-                                        "Variable introduced in bvToInt "
-                                        "pass instead of original variable "
-                                            + original.toString());
-        uint64_t bvsize = original.getType().getBitVectorSize();
-        translation = newVar;
-        d_rangeAssertions.insert(mkRangeConstraint(newVar, bvsize));
-        defineBVUFAsIntUF(original, newVar);
-      }
-    }
-    else if (original.getType().isFunction())
-    {
-      translation = translateFunctionSymbol(original);
-    }
-    else
-    {
-      // variables other than bit-vector variables and function symbols
-      // are left intact
-      translation = original;
-    }
-  }
-  else
-  {
-    // original is a const
-    if (original.getKind() == kind::CONST_BITVECTOR)
-    {
-      // Bit-vector constants are transformed into their integer value.
-      BitVector constant(original.getConst<BitVector>());
-      Integer c = constant.toInteger();
-      translation = d_nm->mkConst(CONST_RATIONAL, Rational(c));
-    }
-    else
-    {
-      // Other constants stay the same.
-      translation = original;
-    }
-  }
-  return translation;
-}
-
-Node BVToInt::translateFunctionSymbol(Node bvUF)
-{
-  // construct the new function symbol.
-  Node intUF;
-  TypeNode tn = bvUF.getType();
-  TypeNode bvRange = tn.getRangeType();
-  // The function symbol has not been converted yet
-  vector<TypeNode> bvDomain = tn.getArgTypes();
-  vector<TypeNode> intDomain;
-  /**
-   * if the original range is a bit-vector sort,
-   * the new range should be an integer sort.
-   * Otherwise, we keep the original range.
-   * Similarly for the domains.
-   */
-  TypeNode intRange = bvRange.isBitVector() ? d_nm->integerType() : bvRange;
-  for (TypeNode d : bvDomain)
-  {
-    intDomain.push_back(d.isBitVector() ? d_nm->integerType() : d);
-  }
-  SkolemManager* sm = d_nm->getSkolemManager();
-  ostringstream os;
-  os << "__bvToInt_fun_" << bvUF << "_int";
-  intUF = sm->mkDummySkolem(
-      os.str(), d_nm->mkFunctionType(intDomain, intRange), "bv2int function");
-  // introduce a `define-fun` in the smt-engine to keep
-  // the correspondence between the original
-  // function symbol and the new one.
-  defineBVUFAsIntUF(bvUF, intUF);
-  return intUF;
-}
-
-void BVToInt::defineBVUFAsIntUF(Node bvUF, Node intUF)
-{
-  // The resulting term
-  Node result;
-  // The type of the resulting term
-  TypeNode resultType;
-  // symbolic arguments of original function
-  vector<Node> args;
-  if (!bvUF.getType().isFunction()) {
-    // bvUF is a variable.
-    // in this case, the result is just the original term
-    // (it will be casted later if needed)
-    result = intUF;
-    resultType = bvUF.getType();
-  } else {
-    // bvUF is a function with arguments
-    // The arguments need to be casted as well.
-    TypeNode tn = bvUF.getType();
-    resultType = tn.getRangeType();
-    vector<TypeNode> bvDomain = tn.getArgTypes();
-    // children of the new symbolic application
-    vector<Node> achildren;
-    achildren.push_back(intUF);
-    int i = 0;
-    for (const TypeNode& d : bvDomain)
-    {
-      // Each bit-vector argument is casted to a natural number
-      // Other arguments are left intact.
-      Node fresh_bound_var = d_nm->mkBoundVar(d);
-      args.push_back(fresh_bound_var);
-      Node castedArg = args[i];
-      if (d.isBitVector())
-      {
-        castedArg = castToType(castedArg, d_nm->integerType());
-      }
-      achildren.push_back(castedArg);
-      i++;
-    }
-    result = d_nm->mkNode(kind::APPLY_UF, achildren);
-  }
-  // If the result is BV, it needs to be casted back.
-  result = castToType(result, resultType);
-  // add the substitution to the preprocessing context, which ensures the
-  // model for bvUF is correct, as well as substituting it in the input
-  // assertions when necessary.
-  if (!args.empty())
-  {
-    result = d_nm->mkNode(
-        kind::LAMBDA, d_nm->mkNode(kind::BOUND_VAR_LIST, args), result);
-  }
-  d_preprocContext->addSubstitution(bvUF, result);
-}
-
-bool BVToInt::childrenTypesChanged(Node n)
-{
-  bool result = false;
-  for (const Node& child : n)
-  {
-    TypeNode originalType = child.getType();
-    TypeNode newType = d_bvToIntCache[child].get().getType();
-    if (!newType.isSubtypeOf(originalType))
-    {
-      result = true;
-      break;
-    }
-  }
-  return result;
-}
-
-Node BVToInt::castToType(Node n, TypeNode tn)
-{
-  // If there is no reason to cast, return the
-  // original node.
-  if (n.getType().isSubtypeOf(tn))
-  {
-    return n;
-  }
-  // We only case int to bv or vice verse.
-  Assert((n.getType().isBitVector() && tn.isInteger())
-         || (n.getType().isInteger() && tn.isBitVector()));
-  if (n.getType().isInteger())
-  {
-    Assert(tn.isBitVector());
-    unsigned bvsize = tn.getBitVectorSize();
-    Node intToBVOp = d_nm->mkConst<IntToBitVector>(IntToBitVector(bvsize));
-    return d_nm->mkNode(intToBVOp, n);
-  }
-  Assert(n.getType().isBitVector());
-  Assert(tn.isInteger());
-  return d_nm->mkNode(kind::BITVECTOR_TO_NAT, n);
-}
-
-Node BVToInt::reconstructNode(Node originalNode,
-                              TypeNode resultType,
-                              const vector<Node>& translated_children)
-{
-  // first, we adjust the children of the node as needed.
-  // re-construct the term with the adjusted children.
-  kind::Kind_t oldKind = originalNode.getKind();
-  NodeBuilder builder(oldKind);
-  if (originalNode.getMetaKind() == kind::metakind::PARAMETERIZED)
-  {
-    builder << originalNode.getOperator();
-  }
-  for (size_t i = 0; i < originalNode.getNumChildren(); i++)
-  {
-    Node originalChild = originalNode[i];
-    Node translatedChild = translated_children[i];
-    Node adjustedChild = castToType(translatedChild, originalChild.getType());
-    builder << adjustedChild;
-  }
-  Node reconstruction = builder.constructNode();
-  // cast to tn in case the reconstruction is a bit-vector.
-  reconstruction = castToType(reconstruction, resultType);
-  return reconstruction;
-}
-
 BVToInt::BVToInt(PreprocessingPassContext* preprocContext)
     : PreprocessingPass(preprocContext, "bv-to-int"),
-      d_binarizeCache(userContext()),
-      d_eliminationCache(userContext()),
-      d_rebuildCache(userContext()),
-      d_bvToIntCache(userContext()),
-      d_rangeAssertions(userContext())
-{
-  d_nm = NodeManager::currentNM();
-  d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0));
-  d_one = d_nm->mkConst(CONST_RATIONAL, Rational(1));
-
-  if (options().smt.solveBVAsInt == options::SolveBVAsIntMode::BITWISE)
-  {
-    throw OptionException("bitwise option is not supported currently");
-  }
-};
+      d_intBlaster(preprocContext->getEnv(),
+                   options::solveBVAsInt(),
+                   options::BVAndIntegerGranularity()) {}
 
 PreprocessingPassResult BVToInt::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
+  // vector of boolean nodes for additional constraints
+  // this will always contain range constraints
+  // and for options::SolveBVAsIntMode::BITWISE, it will
+  // also include bitwise assertion constraints
+  std::vector<Node> additionalConstraints;
+  std::map<Node, Node> skolems;
   for (uint64_t i = 0; i < assertionsToPreprocess->size(); ++i)
   {
     Node bvNode = (*assertionsToPreprocess)[i];
-    Node intNode = bvToInt(bvNode);
+    Node intNode =
+        d_intBlaster.intBlast(bvNode, additionalConstraints, skolems);
     Node rwNode = rewrite(intNode);
     Trace("bv-to-int-debug") << "bv node: " << bvNode << std::endl;
     Trace("bv-to-int-debug") << "int node: " << intNode << std::endl;
     Trace("bv-to-int-debug") << "rw node: " << rwNode << std::endl;
     assertionsToPreprocess->replace(i, rwNode);
   }
-  addFinalizeRangeAssertions(assertionsToPreprocess);
+  addFinalizeAssertions(assertionsToPreprocess, additionalConstraints);
+  addSkolemDefinitions(skolems);
   return PreprocessingPassResult::NO_CONFLICT;
 }
 
-void BVToInt::addFinalizeRangeAssertions(
-    AssertionPipeline* assertionsToPreprocess)
-{
-  // collect the range assertions from d_rangeAssertions
-  // (which is a context-dependent set)
-  // into a vector.
-  vector<Node> vec_range;
-  vec_range.assign(d_rangeAssertions.key_begin(), d_rangeAssertions.key_end());
-  // conjoin all range assertions and add the conjunction
-  // as a new assertion
-  Node rangeAssertions = rewrite(d_nm->mkAnd(vec_range));
-  assertionsToPreprocess->push_back(rangeAssertions);
-  Trace("bv-to-int-debug") << "range constraints: "
-                           << rangeAssertions.toString() << std::endl;
-}
-
-Node BVToInt::createShiftNode(vector<Node> children,
-                              uint64_t bvsize,
-                              bool isLeftShift)
-{
-  /**
-   * from SMT-LIB:
-   * [[(bvshl s t)]] := nat2bv[m](bv2nat([[s]]) * 2^(bv2nat([[t]])))
-   * [[(bvlshr s t)]] := nat2bv[m](bv2nat([[s]]) div 2^(bv2nat([[t]])))
-   * Since we don't have exponentiation, we use an ite.
-   * Important note: below we use INTS_DIVISION_TOTAL, which is safe here
-   * because we divide by 2^... which is never 0.
-   */
-  Node x = children[0];
-  Node y = children[1];
-  // shifting by const is eliminated by the theory rewriter
-  Assert(!y.isConst());
-  Node ite = d_zero;
-  Node body;
-  for (uint64_t i = 0; i < bvsize; i++)
-  {
-    if (isLeftShift)
-    {
-      body = d_nm->mkNode(kind::INTS_MODULUS_TOTAL,
-                          d_nm->mkNode(kind::MULT, x, pow2(i)),
-                          pow2(bvsize));
-    }
-    else
-    {
-      body = d_nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i));
-    }
-    ite = d_nm->mkNode(
-        kind::ITE,
-        d_nm->mkNode(
-            kind::EQUAL, y, d_nm->mkConst(CONST_RATIONAL, Rational(i))),
-        body,
-        ite);
-  }
-  return ite;
-}
-
-Node BVToInt::translateQuantifiedFormula(Node quantifiedNode)
+void BVToInt::addSkolemDefinitions(const std::map<Node, Node>& skolems)
 {
-  kind::Kind_t k = quantifiedNode.getKind();
-  Node boundVarList = quantifiedNode[0];
-  Assert(boundVarList.getKind() == kind::BOUND_VAR_LIST);
-  // Since bit-vector variables are being translated to
-  // integer variables, we need to substitute the new ones
-  // for the old ones.
-  vector<Node> oldBoundVars;
-  vector<Node> newBoundVars;
-  vector<Node> rangeConstraints;
-  for (Node bv : quantifiedNode[0])
+  map<Node, Node>::const_iterator it;
+  for (it = skolems.begin(); it != skolems.end(); it++)
   {
-    oldBoundVars.push_back(bv);
-    if (bv.getType().isBitVector())
+    Node originalSkolem = it->first;
+    Node definition = it->second;
+    std::vector<Node> args;
+    Node body;
+    if (definition.getType().isFunction())
     {
-      // bit-vector variables are replaced by integer ones.
-      // the new variables induce range constraints based on the
-      // original bit-width.
-      Node newBoundVar = d_bvToIntCache[bv];
-      newBoundVars.push_back(newBoundVar);
-      rangeConstraints.push_back(
-          mkRangeConstraint(newBoundVar, bv.getType().getBitVectorSize()));
+      args.insert(args.end(), definition[0].begin(), definition[0].end());
+      body = definition[1];
     }
     else
     {
-      // variables that are not bit-vectors are not changed
-      newBoundVars.push_back(bv);
+      body = definition;
     }
+    Trace("bv-to-int-debug") << "adding substitution: " << "[" << originalSkolem  << "] ----> [" << definition << "]"  << std::endl; 
+    d_preprocContext->addSubstitution(originalSkolem, definition);
   }
-
-  // the body of the quantifier
-  Node matrix = d_bvToIntCache[quantifiedNode[1]];
-  // make the substitution
-  matrix = matrix.substitute(oldBoundVars.begin(),
-                             oldBoundVars.end(),
-                             newBoundVars.begin(),
-                             newBoundVars.end());
-  // A node to represent all the range constraints.
-  Node ranges = d_nm->mkAnd(rangeConstraints);
-  // Add the range constraints to the body of the quantifier.
-  // For "exists", this is added conjunctively
-  // For "forall", this is added to the left side of an implication.
-  matrix = d_nm->mkNode(
-      k == kind::FORALL ? kind::IMPLIES : kind::AND, ranges, matrix);
-  // create the new quantified formula and return it.
-  Node newBoundVarsList = d_nm->mkNode(kind::BOUND_VAR_LIST, newBoundVars);
-  Node result = d_nm->mkNode(kind::FORALL, newBoundVarsList, matrix);
-  return result;
 }
 
-Node BVToInt::createBVNotNode(Node n, uint64_t bvsize)
+void BVToInt::addFinalizeAssertions(
+    AssertionPipeline* assertionsToPreprocess,
+    const std::vector<Node>& additionalConstraints)
 {
-  return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n);
+  NodeManager* nm = NodeManager::currentNM();
+  Node lemmas = nm->mkAnd(additionalConstraints);
+  assertionsToPreprocess->push_back(lemmas);
+  Trace("bv-to-int-debug") << "range constraints: " << lemmas.toString()
+                           << std::endl;
 }
 
 }  // namespace passes
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
index d09f9e738..24fc185b5 100644
--- a/src/preprocessing/passes/bv_to_int.h
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -1,6 +1,7 @@
+
 /******************************************************************************
  * Top contributors (to current version):
- *   Yoni Zohar, Gereon Kremer, Makai Mann
+ *   Yoni Zohar
  *
  * This file is part of the cvc5 project.
  *
@@ -10,69 +11,18 @@
  * directory for licensing information.
  * ****************************************************************************
  *
- * The BVToInt preprocessing pass
- *
- * Converts bit-vector formulas to integer formulas.
- * The conversion is implemented using a translation function Tr,
- * roughly described as follows:
- *
- * Tr(x) = fresh_x for every bit-vector variable x, where fresh_x is a fresh
- *         integer variable.
- * Tr(c) = the integer value of c, for any bit-vector constant c.
- * Tr((bvadd s t)) = Tr(s) + Tr(t) mod 2^k, where k is the bit width of
- *         s and t.
- * Similar transformations are done for bvmul, bvsub, bvudiv, bvurem, bvneg,
- *         bvnot, bvconcat, bvextract
- * Tr((_ zero_extend m) x) = Tr(x)
- * Tr((_ sign_extend m) x) = ite(msb(x)=0, x, 2^k*(2^m-1) + x))
- * explanation: if the msb is 0, this is the same as zero_extend,
- * which does not change the integer value.
- * If the msb is 1, then the result should correspond to
- * concat(1...1, x), with m 1's.
- * m 1's is 2^m-1, and multiplying it by x's width (k) moves it
- * to the front.
- *
- * Tr((bvand s t)) depends on the granularity, which is provided by the user
- * when enabling this preprocessing pass.
- * We divide s and t to blocks.
- * The size of each block is the granularity, and so the number of
- * blocks is:
- * bit width/granularity (rounded down).
- * We create an ITE that represents an arbitrary block,
- * and then create a sum by mutiplying each block by the
- * appropriate power of two.
- * More formally:
- * Let g denote the granularity.
- * Let k denote the bit width of s and t.
- * Let b denote floor(k/g) if k >= g, or just k otherwise.
- * Tr((bvand s t)) =
- * Sigma_{i=0}^{b-1}(bvand s[(i+1)*g, i*g] t[(i+1)*g, i*g])*2^(i*g)
- *
- * Similar transformations are done for bvor, bvxor, bvxnor, bvnand, bvnor.
- *
- * Tr((bvshl a b)) = ite(Tr(b) >= k, 0, Tr(a)*ITE), where k is the bit width of
- *         a and b, and ITE represents exponentiation up to k, that is:
- * ITE = ite(Tr(b)=0, 1, ite(Tr(b)=1), 2, ite(Tr(b)=2, 4, ...))
- * Similar transformations are done for bvlshr.
- *
- * Tr(a=b) = Tr(a)=Tr(b)
- * Tr((bvult a b)) = Tr(a) < Tr(b)
- * Similar transformations are done for bvule, bvugt, and bvuge.
- *
- * Bit-vector operators that are not listed above are either eliminated using
- * the function eliminationPass, or are not supported.
- *
+ * The bv-to-int preprocessing pass.
  */
 
-#include "cvc5_private.h"
-
 #ifndef __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H
 #define __CVC5__PREPROCESSING__PASSES__BV_TO_INT_H
 
 #include "context/cdhashmap.h"
-#include "context/cdhashset.h"
+#include "context/cdo.h"
+#include "context/context.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "theory/arith/nl/iand_utils.h"
+#include "preprocessing/preprocessing_pass_context.h"
+#include "theory/bv/int_blaster.h"
 
 namespace cvc5 {
 namespace preprocessing {
@@ -88,200 +38,15 @@ class BVToInt : public PreprocessingPass
  protected:
   PreprocessingPassResult applyInternal(
       AssertionPipeline* assertionsToPreprocess) override;
-  /**
-   * A generic function that creates a logical shift node (either left or
-   * right). a << b gets translated to a * 2^b mod 2^k, where k is the bit
-   * width. a >> b gets translated to a div 2^b mod 2^k, where k is the bit
-   * width. The exponentiation operation is translated to an ite for possible
-   * values of the exponent, from 0 to k-1.
-   * If the right operand of the shift is greater than k-1,
-   * the result is 0.
-   * @param children the two operands for the shift
-   * @param bvsize the original bit widths of the operands
-   *                (before translation to integers)
-   * @param  isLeftShift true iff the desired operation is a left shift.
-   * @return a node representing the shift.
-   *
-   */
-  Node createShiftNode(std::vector<Node> children,
-                       uint64_t bvsize,
-                       bool isLeftShift);
-
-  /**
-   * Returns a node that represents the bitwise negation of n.
-   */
-  Node createBVNotNode(Node n, uint64_t bvsize);
-
-  /**
-   * The result is an integer term and is computed
-   * according to the translation specified above.
-   * @param n is a bit-vector term or formula to be translated.
-   * @return integer node that corresponds to n.
-   */
-  Node bvToInt(Node n);
-
-  /**
-   * Whenever we introduce an integer variable that represents a bit-vector
-   * variable, we need to guard the range of the newly introduced variable.
-   * For bit width k, the constraint is 0 <= newVar < 2^k.
-   * @param newVar the newly introduced integer variable
-   * @param k the bit width of the original bit-vector variable.
-   * @return a node representing the range constraint.
-   */
-  Node mkRangeConstraint(Node newVar, uint64_t k);
-
-  /**
-   * In the translation to integers, it is convenient to assume that certain
-   * bit-vector operators do not occur in the original formula (e.g., repeat).
-   * This function eliminates all these operators.
-   */
-  Node eliminationPass(Node n);
-
-  /**
-   * Some bit-vector operators (e.g., bvadd, bvand) are binary, but allow more
-   * than two arguments as a syntactic sugar.
-   * For example, we can have a node for (bvand x y z), 
-   * that represents (bvand (x (bvand y z))).
-   * This function makes all such operators strictly binary.
-   */
-  Node makeBinary(Node n);
-
-  /**
-   * @param k A non-negative integer
-   * @return A node that represents the constant 2^k
-   */
-  Node pow2(uint64_t k);
-
-  /**
-   * @param k A positive integer k
-   * @return A node that represent the constant 2^k-1
-   * For example, if k is 4, the result is a node representing the
-   * constant 15.
-   */
-  Node maxInt(uint64_t k);
-
-  /**
-   * @param n A node representing an integer term
-   * @param exponent A non-negative integer
-   * @return A node representing (n mod (2^exponent))
-   */
-  Node modpow2(Node n, uint64_t exponent);
-
-  bool childrenTypesChanged(Node n);
-
-  /**
-   * Add the range assertions collected in d_rangeAssertions
-   * (using mkRangeConstraint) to the assertion pipeline.
-   * If there are no range constraints, do nothing.
-   * If there is a single range constraint, add it to the pipeline.
-   * Otherwise, add all of them as a single conjunction
-   */
-  void addFinalizeRangeAssertions(AssertionPipeline* assertionsToPreprocess);
-
-  /**
-   * @param quantifiedNode a node whose main operator is forall/exists.
-   * @return a node opbtained from quantifiedNode by:
-   * 1. Replacing all bound BV variables by new bound integer variables.
-   * 2. Add range constraints for the new variables, induced by the original
-   * bit-width. These range constraints are added with "AND" in case of exists
-   * and with "IMPLIES" in case of forall.
-   */
-  Node translateQuantifiedFormula(Node quantifiedNode);
-
-  /**
-   * Reconstructs a node whose main operator cannot be
-   * translated to integers.
-   * Reconstruction is done by casting to integers/bit-vectors
-   * as needed.
-   * For example, if node is (select A x) where A
-   * is a bit-vector array, we do not change A to be
-   * an integer array, even though x was translated
-   * to integers.
-   * In this case we cast x to (bv2nat x) during
-   * the reconstruction.
-   *
-   * @param originalNode the node that we are reconstructing
-   * @param resultType the desired type for the reconstruction
-   * @param translated_children the children of originalNode
-   *        after their translation to integers.
-   * @return A node with originalNode's operator that has type resultType.
-   */
-  Node reconstructNode(Node originalNode,
-                       TypeNode resultType,
-                       const std::vector<Node>& translated_children);
-
-  /**
-   * A useful utility function.
-   * if n is an integer and tn is bit-vector,
-   * applies the IntToBitVector operator on n.
-   * if n is a vit-vector and tn is integer,
-   * applies BitVector_TO_NAT operator.
-   * Otherwise, keeps n intact.
-   */
-  Node castToType(Node n, TypeNode tn);
-
-  /**
-   * When a UF f is translated to a UF g,
-   * we add a define-fun command to the smt-engine
-   * to relate between f and g.
-   * We do the same when f and g are just variables.
-   * This is useful, for example, when asking
-   * for a model-value of a term that includes the
-   * original UF f.
-   * @param bvUF the original function or variable
-   * @param intUF the translated function or variable
-   */
-  void defineBVUFAsIntUF(Node bvUF, Node intUF);
-
-  /**
-   * @param bvUF is an uninterpreted function symbol from the original formula
-   * @return a fresh uninterpreted function symbol, obtained from bvUF
-     by replacing every argument of type BV to an argument of type Integer,
-     and the return type becomes integer in case it was BV.
-   */
-  Node translateFunctionSymbol(Node bvUF);
-
-  /**
-   * Performs the actual translation to integers for nodes
-   * that have children.
-   */
-  Node translateWithChildren(Node original,
-                             const std::vector<Node>& translated_children);
-
-  /**
-   * Performs the actual translation to integers for nodes
-   * that don't have children (variables, constants, uninterpreted function
-   * symbols).
-   */
-  Node translateNoChildren(Node original);
-
-  /**
-   * Caches for the different functions
-   */
-  CDNodeMap d_binarizeCache;
-  CDNodeMap d_eliminationCache;
-  CDNodeMap d_rebuildCache;
-  CDNodeMap d_bvToIntCache;
 
-  /**
-   * Node manager that is used throughout the pass
-   */
-  NodeManager* d_nm;
+  // Add the lemmas in `additionalConstraints` to the assertions pipeline.
+  void addFinalizeAssertions(AssertionPipeline* assertionsToPreprocess,
+                             const std::vector<Node>& additionalConstraints);
 
-  /**
-   * A set of constraints of the form 0 <= x < 2^k
-   * These are added for every new integer variable that we introduce.
-   */
-  context::CDHashSet<Node> d_rangeAssertions;
+  // include the skolem map as substitutions
+  void addSkolemDefinitions(const std::map<Node, Node>& skolems);
 
-  /**
-   * Useful constants
-   */
-  Node d_zero;
-  Node d_one;
-  
-  /** helper class for handeling bvand translation */
-  theory::arith::nl::IAndUtils d_iandUtils;
+  IntBlaster d_intBlaster;
 };
 
 }  // namespace passes
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index f5e7b427e..4c01f25f3 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -402,11 +402,11 @@ RewriteResponse ArithRewriter::postRewritePow2(TNode t)
 RewriteResponse ArithRewriter::postRewriteIAnd(TNode t)
 {
   Assert(t.getKind() == kind::IAND);
+  size_t bsize = t.getOperator().getConst<IntAnd>().d_size;
   NodeManager* nm = NodeManager::currentNM();
   // if constant, we eliminate
   if (t[0].isConst() && t[1].isConst())
   {
-    size_t bsize = t.getOperator().getConst<IntAnd>().d_size;
     Node iToBvop = nm->mkConst(IntToBitVector(bsize));
     Node arg1 = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvop, t[0]);
     Node arg2 = nm->mkNode(kind::INT_TO_BITVECTOR, iToBvop, t[1]);
@@ -437,6 +437,11 @@ RewriteResponse ArithRewriter::postRewriteIAnd(TNode t)
       // ((_ iand k) 0 y) ---> 0
       return RewriteResponse(REWRITE_DONE, t[i]);
     }
+    if (t[i].getConst<Rational>().getNumerator() == Integer(2).pow(bsize) - 1)
+    {
+      // ((_ iand k) 111...1 y) ---> y
+      return RewriteResponse(REWRITE_DONE, t[i == 0 ? 1 : 0]);
+    }
   }
   return RewriteResponse(REWRITE_DONE, t);
 }
diff --git a/src/theory/arith/nl/iand_solver.cpp b/src/theory/arith/nl/iand_solver.cpp
index 90a9c5f78..92ecaf4e8 100644
--- a/src/theory/arith/nl/iand_solver.cpp
+++ b/src/theory/arith/nl/iand_solver.cpp
@@ -280,8 +280,8 @@ Node IAndSolver::bitwiseLemma(Node i)
   // compare each bit to bvI
   Node cond;
   Node bitIAnd;
-  unsigned high_bit;
-  for (unsigned j = 0; j < bvsize; j += granularity)
+  uint64_t high_bit;
+  for (uint64_t j = 0; j < bvsize; j += granularity)
   {
     high_bit = j + granularity - 1;
     // don't let high_bit pass bvsize
diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index 692fdc1b3..60bb0a9bc 100644
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -48,8 +48,7 @@ Rational intpow2(uint64_t b) { return Rational(Integer(2).pow(b), Integer(1)); }
 
 IntBlaster::IntBlaster(Env& env,
                        options::SolveBVAsIntMode mode,
-                       uint64_t granularity,
-                       bool introduceFreshIntVars)
+                       uint64_t granularity)
     : EnvObj(env),
       d_binarizeCache(userContext()),
       d_intblastCache(userContext()),
@@ -57,8 +56,7 @@ IntBlaster::IntBlaster(Env& env,
       d_bitwiseAssertions(userContext()),
       d_mode(mode),
       d_granularity(granularity),
-      d_context(userContext()),
-      d_introduceFreshIntVars(introduceFreshIntVars)
+      d_context(userContext())
 {
   d_nm = NodeManager::currentNM();
   d_zero = d_nm->mkConst(CONST_RATIONAL, Rational(0));
@@ -678,38 +676,18 @@ Node IntBlaster::translateNoChildren(Node original,
       }
       else
       {
-        // original is a bit-vector variable (symbolic constant).
-        // Either we translate it to a fresh integer variable,
-        // or we translate it to (bv2nat original).
-        // In the former case, we must include range lemmas, while in the
-        // latter we don't.
-        // This is determined by the option bv-to-int-fresh-vars.
-        // The variables intCast and bvCast are used for models:
-        // even if we introduce a fresh variable,
-        // it is associated with intCast (which is (bv2nat original)).
-        // bvCast is either ( (_ nat2bv k) original) or just original.
         Node intCast = castToType(original, d_nm->integerType());
         Node bvCast;
-        if (d_introduceFreshIntVars)
-        {
-          // we introduce a fresh variable, add range constraints, and save the
-          // connection between original and the new variable via intCast
-          translation = d_nm->getSkolemManager()->mkPurifySkolem(
-              intCast,
-              "__intblast__var",
-              "Variable introduced in intblasting for " + original.toString());
-          uint64_t bvsize = original.getType().getBitVectorSize();
-          addRangeConstraint(translation, bvsize, lemmas);
-          // put new definition of old variable in skolems
-          bvCast = castToType(translation, original.getType());
-        }
-        else
-        {
-          // we just translate original to (bv2nat original)
-          translation = intCast;
-          // no need to do any casting back to bit-vector in this case.
-          bvCast = original;
-        }
+        // we introduce a fresh variable, add range constraints, and save the
+        // connection between original and the new variable via intCast
+        translation = d_nm->getSkolemManager()->mkPurifySkolem(
+            intCast,
+            "__intblast__var",
+            "Variable introduced in intblasting for " + original.toString());
+        uint64_t bvsize = original.getType().getBitVectorSize();
+        addRangeConstraint(translation, bvsize, lemmas);
+        // put new definition of old variable in skolems
+        bvCast = castToType(translation, original.getType());
 
         // add bvCast to skolems if it is not already there.
         if (skolems.find(original) == skolems.end())
diff --git a/src/theory/bv/int_blaster.h b/src/theory/bv/int_blaster.h
index ed8ed10c6..fb7291f6e 100644
--- a/src/theory/bv/int_blaster.h
+++ b/src/theory/bv/int_blaster.h
@@ -101,14 +101,12 @@ class IntBlaster : protected EnvObj
    * @param context user context
    * @param mode bv-to-int translation mode
    * @param granularity bv-to-int translation granularity
-   * @param introduceFreshIntVars determines whether bit-vector variables are
    * translated to integer variables, or are directly casted using `bv2nat`
    * operator. not purely bit-vector nodes.
    */
   IntBlaster(Env& env,
              options::SolveBVAsIntMode mode,
-             uint64_t granluarity = 1,
-             bool introduceFreshIntVars = true);
+             uint64_t granluarity = 1);
 
   ~IntBlaster();
 
@@ -371,11 +369,6 @@ class IntBlaster : protected EnvObj
   /** an SolverEngine for context */
   context::Context* d_context;
 
-  /** true iff the translator should introduce
-   * fresh integer variables for bit-vector variables.
-   * Otherwise, we introduce a nat2bv term.
-   */
-  bool d_introduceFreshIntVars;
 };
 
 }  // namespace cvc5
diff --git a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
index 496a625ee..a8ac27a81 100644
--- a/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
+++ b/src/theory/bv/theory_bv_rewrite_rules_operator_elimination.h
@@ -29,84 +29,6 @@ namespace cvc5 {
 namespace theory {
 namespace bv {
 
-/*
- * This rewrite is not meant to be used by the BV rewriter.
- * It is specifically designed for the bv-to-int preprocessing pass.
- * Based on Hacker's Delight section 2-2 equation a:
- * -x = ~x+1
- */
-template <>
-inline bool RewriteRule<NegEliminate>::applies(TNode node)
-{
-  return (node.getKind() == kind::BITVECTOR_NEG);
-}
-
-template <>
-inline Node RewriteRule<NegEliminate>::apply(TNode node)
-{
-  Debug("bv-rewrite") << "RewriteRule<NegEliminate>(" << node << ")"
-                      << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
-  TNode a = node[0];
-  unsigned size = utils::getSize(a);
-  Node one = utils::mkOne(size);
-  Node nota = nm->mkNode(kind::BITVECTOR_NOT, a);
-  Node bvadd = nm->mkNode(kind::BITVECTOR_ADD, nota, one);
-  return bvadd;
-}
-
-/*
- * This rewrite is not meant to be used by the BV rewriter.
- * It is specifically designed for the bv-to-int preprocessing pass.
- * Based on Hacker's Delight section 2-2 equation h:
- * x+y = x|y + x&y
- */
-template <>
-inline bool RewriteRule<OrEliminate>::applies(TNode node)
-{
-  return (node.getKind() == kind::BITVECTOR_OR);
-}
-
-template <>
-inline Node RewriteRule<OrEliminate>::apply(TNode node)
-{
-  Debug("bv-rewrite") << "RewriteRule<OrEliminate>(" << node << ")"
-                      << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
-  TNode a = node[0];
-  TNode b = node[1];
-  Node bvadd = nm->mkNode(kind::BITVECTOR_ADD, a, b);
-  Node bvand = nm->mkNode(kind::BITVECTOR_AND, a, b);
-  Node result =
-      nm->mkNode(kind::BITVECTOR_SUB, bvadd, bvand);
-  return result;
-}
-
-/*
- * This rewrite is not meant to be used by the BV rewriter.
- * It is specifically designed for the bv-to-int preprocessing pass.
- * Based on Hacker's Delight section 2-2 equation n:
- * x xor y = x|y - x&y
- */
-template <>
-inline bool RewriteRule<XorEliminate>::applies(TNode node)
-{
-  return (node.getKind() == kind::BITVECTOR_XOR);
-}
-
-template <>
-inline Node RewriteRule<XorEliminate>::apply(TNode node)
-{
-  Debug("bv-rewrite") << "RewriteRule<XorEliminate>(" << node << ")"
-                      << std::endl;
-  NodeManager* nm = NodeManager::currentNM();
-  TNode a = node[0];
-  TNode b = node[1];
-  Node bvor = nm->mkNode(kind::BITVECTOR_OR, a, b);
-  Node bvand = nm->mkNode(kind::BITVECTOR_AND, a, b);
-  Node result = nm->mkNode(kind::BITVECTOR_SUB, bvor, bvand);
-  return result;
-}
 
 template <>
 inline bool RewriteRule<UgtEliminate>::applies(TNode node)
diff --git a/test/api/cpp/CMakeLists.txt b/test/api/cpp/CMakeLists.txt
index eae57f3b9..929c5bef2 100644
--- a/test/api/cpp/CMakeLists.txt
+++ b/test/api/cpp/CMakeLists.txt
@@ -54,3 +54,5 @@ cvc5_add_api_test(issue4889)
 cvc5_add_api_test(issue6111)
 cvc5_add_api_test(proj-issue306)
 cvc5_add_api_test(proj-issue334)
+cvc5_add_api_test(proj-issue344)
+cvc5_add_api_test(proj-issue345)
diff --git a/test/api/cpp/proj-issue344.cpp b/test/api/cpp/proj-issue344.cpp
new file mode 100644
index 000000000..5f486706c
--- /dev/null
+++ b/test/api/cpp/proj-issue344.cpp
@@ -0,0 +1,33 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Yoni Zohar
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Test for project issue #345
+ *
+ */
+
+
+#include "api/cpp/cvc5.h"
+#include <cassert>
+
+using namespace cvc5::api;
+
+int main(void)
+{
+  Solver slv;
+  slv.setOption("solve-bv-as-int", "iand");
+  Sort s12 = slv.getIntegerSort();
+  Term t13 = slv.mkConst(s12, "_x11");
+  Term t25 = slv.mkTerm(slv.mkOp(Kind::INT_TO_BITVECTOR, 4124876294), {t13});
+  Term t66 = slv.mkTerm(Kind::BITVECTOR_ULTBV, {t25, t25});
+  Term t154 = slv.mkTerm(Kind::BITVECTOR_SGT, {t66, t66});
+  slv.checkEntailed({t154, t154, t154, t154});
+}
diff --git a/test/api/cpp/proj-issue345.cpp b/test/api/cpp/proj-issue345.cpp
new file mode 100644
index 000000000..c33e9e5b8
--- /dev/null
+++ b/test/api/cpp/proj-issue345.cpp
@@ -0,0 +1,34 @@
+/******************************************************************************
+ * Top contributors (to current version):
+ *   Yoni Zohar
+ *
+ * This file is part of the cvc5 project.
+ *
+ * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
+ * in the top-level source directory and their institutional affiliations.
+ * All rights reserved.  See the file COPYING in the top-level source
+ * directory for licensing information.
+ * ****************************************************************************
+ *
+ * Test for project issue #345
+ *
+ */
+
+
+#include "api/cpp/cvc5.h"
+#include <cassert>
+
+using namespace cvc5::api;
+
+int main(void)
+{
+  Solver slv;
+  slv.setOption("solve-bv-as-int", "iand");
+  Sort s12 = slv.getIntegerSort();
+  Term t13 = slv.mkConst(s12, "_x11");
+  Term t25 = slv.mkTerm(slv.mkOp(Kind::INT_TO_BITVECTOR, 4124876294), {t13});
+  Term t66 = slv.mkTerm(Kind::BITVECTOR_SLTBV, {t25, t25});
+  Term t154 = slv.mkTerm(Kind::BITVECTOR_SGT, {t66, t66});
+  slv.checkEntailed({t154, t154, t154, t154});
+}
+
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6b8debc88..3be63c46d 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -257,6 +257,7 @@ set(regress_0_tests
   regress0/bv/bv_to_int_bvuf_to_intuf.smt2
   regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
   regress0/bv/bv_to_int_elim_err.smt2
+  regress0/bv/bv_to_int_int1.smt2
   regress0/bv/bv_to_int_zext.smt2
   regress0/bv/bvcomp.cvc.smt2
   regress0/bv/bvmul-pow2-only.smt2
@@ -434,6 +435,7 @@ set(regress_0_tests
   regress0/bv/mult-pow2-negative.smt2
   regress0/bv/pr4993-bvugt-bvurem-a.smt2
   regress0/bv/pr4993-bvugt-bvurem-b.smt2
+  regress0/bv/proj-issue343.smt2
   regress0/bv/reset-assertions-assert-input.smt2
   regress0/bv/sizecheck.cvc.smt2
   regress0/bv/smtcompbug.smtv1.smt2
@@ -2627,6 +2629,7 @@ set(regress_2_tests
   regress2/bv_to_int_mask_array_2.smt2
   regress2/bv_to_int_mask_array_3.smt2
   regress2/bv_to_int_shifts.smt2
+  regress2/bv_to_int_quantifiers_bvand.smt2
   regress2/error1.smtv1.smt2
   regress2/fp/issue7056.smt2
   regress2/fuzz_2.smtv1.smt2
diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2
index 3908cdb16..eb8e75803 100644
--- a/test/regress/regress0/bv/bv_to_int1.smt2
+++ b/test/regress/regress0/bv/bv_to_int1.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun x () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
index 91e0c45fd..eced6e0e9 100644
--- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T4_180 () (_ BitVec 32))
diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
index 3e545ef03..45d539f04 100644
--- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (declare-fun a () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
index 0a0ec7b20..ae77380dd 100644
--- a/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvuf_to_intuf_sorts.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (declare-sort S 0)
diff --git a/test/regress/regress0/bv/bv_to_int_elim_err.smt2 b/test/regress/regress0/bv/bv_to_int_elim_err.smt2
index 01ee5dad8..cb7eefbb2 100644
--- a/test/regress/regress0/bv/bv_to_int_elim_err.smt2
+++ b/test/regress/regress0/bv/bv_to_int_elim_err.smt2
@@ -1,4 +1,5 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1  
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun _substvar_183_ () (_ BitVec 32))
diff --git a/test/regress/regress0/bv/bv_to_int_int1.smt2 b/test/regress/regress0/bv/bv_to_int_int1.smt2
new file mode 100644
index 000000000..3295d3481
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_int1.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; EXPECT: sat
+(set-logic QF_ALL)
+(declare-fun x () (_ BitVec 4))
+(declare-fun y () (_ BitVec 4))
+(declare-fun z () Int)
+(declare-fun w () Int)
+(assert (= x (_ bv3 4)))
+(assert (= y (_ bv3 4)))
+(assert (> z w))
+(check-sat)
diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2
index 8bf4a825d..4fd6109f4 100644
--- a/test/regress/regress0/bv/bv_to_int_zext.smt2
+++ b/test/regress/regress0/bv/bv_to_int_zext.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T1_31078 () (_ BitVec 8))
diff --git a/test/regress/regress0/bv/proj-issue343.smt2 b/test/regress/regress0/bv/proj-issue343.smt2
new file mode 100644
index 000000000..6d2971ad8
--- /dev/null
+++ b/test/regress/regress0/bv/proj-issue343.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+; COMMAND-LINE: --no-check-models
+(set-logic ALL)
+(set-option :solve-bv-as-int bv)
+(declare-const _x8 Real)
+(assert (distinct real.pi _x8))
+(check-sat)
diff --git a/test/regress/regress2/bv_to_int2.smt2 b/test/regress/regress2/bv_to_int2.smt2
index 424e95b27..b9c27c6b8 100644
--- a/test/regress/regress2/bv_to_int2.smt2
+++ b/test/regress/regress2/bv_to_int2.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2
index 0c6768546..1f5df2c31 100644
--- a/test/regress/regress2/bv_to_int_ashr.smt2
+++ b/test/regress/regress2/bv_to_int_ashr.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress2/bv_to_int_bitwise.smt2 b/test/regress/regress2/bv_to_int_bitwise.smt2
index 23624e12c..4dc37a94c 100644
--- a/test/regress/regress2/bv_to_int_bitwise.smt2
+++ b/test/regress/regress2/bv_to_int_bitwise.smt2
@@ -1,8 +1,10 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5
-; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value
-; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum
-; COMMAND-LINE: --solve-bv-as-int=bv
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=5 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun s () (_ BitVec 4))
diff --git a/test/regress/regress2/bv_to_int_bvmul1.smt2 b/test/regress/regress2/bv_to_int_bvmul1.smt2
index 232959f33..bf6f2cfc4 100644
--- a/test/regress/regress2/bv_to_int_bvmul1.smt2
+++ b/test/regress/regress2/bv_to_int_bvmul1.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2 b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
index babf9af32..2ecd0fe6c 100644
--- a/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
+++ b/test/regress/regress2/bv_to_int_bvuf_to_intuf_smtlib.smt2
@@ -1,4 +1,5 @@
-;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-unsat-cores
+;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+;COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores
 ;EXPECT: unsat
 (set-logic QF_UFBV)
 (declare-fun z$n0s32 () (_ BitVec 32))
diff --git a/test/regress/regress2/bv_to_int_inc1.smt2 b/test/regress/regress2/bv_to_int_inc1.smt2
index 4b22c8ed8..28fb86f76 100644
--- a/test/regress/regress2/bv_to_int_inc1.smt2
+++ b/test/regress/regress2/bv_to_int_inc1.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --incremental --solve-bv-as-int=sum
+; COMMAND-LINE: --incremental --solve-bv-as-int=bitwise
 ; COMMAND-LINE: --incremental --solve-bv-as-int=iand
 ; COMMAND-LINE: --incremental --solve-bv-as-int=bv
 ; EXPECT sat
diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2
index 3b55c035d..c12138091 100644
--- a/test/regress/regress2/bv_to_int_mask_array_1.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_1.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
-; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value --no-check-unsat-cores
 ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum --no-check-unsat-cores
 ; COMMAND-LINE: --solve-bv-as-int=bv --no-check-unsat-cores
 ; EXPECT: unsat
diff --git a/test/regress/regress2/bv_to_int_mask_array_2.smt2 b/test/regress/regress2/bv_to_int_mask_array_2.smt2
index edcc14149..17a113f85 100644
--- a/test/regress/regress2/bv_to_int_mask_array_2.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_2.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=value
 ; COMMAND-LINE: --solve-bv-as-int=iand --iand-mode=sum
 ; COMMAND-LINE: --solve-bv-as-int=bv
diff --git a/test/regress/regress2/bv_to_int_mask_array_3.smt2 b/test/regress/regress2/bv_to_int_mask_array_3.smt2
index 74e5ca95a..2b411209d 100644
--- a/test/regress/regress2/bv_to_int_mask_array_3.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_3.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic ALL)
 (declare-fun A () (Array (_ BitVec 4) (_ BitVec 4)))
diff --git a/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2 b/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2
new file mode 100644
index 000000000..d454ad630
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_quantifiers_bvand.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1 --no-check-unsat-cores
+; EXPECT: (error "Error in option parsing: --solve-bv-as-int=bitwise does not support quantifiers")
+; EXIT: 1
+(set-logic BV)
+(declare-const x (_ BitVec 8))
+(assert (forall ((y (_ BitVec 8)))
+               (distinct #b00000000
+                         (bvand x y))))
+(check-sat)
diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2
index bcc31c38c..173f1a552 100644
--- a/test/regress/regress2/bv_to_int_shifts.smt2
+++ b/test/regress/regress2/bv_to_int_shifts.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun s () (_ BitVec 4))
diff --git a/test/regress/regress3/bv_to_int_and_or.smt2 b/test/regress/regress3/bv_to_int_and_or.smt2
index 2c728417d..8ae10a04f 100644
--- a/test/regress/regress3/bv_to_int_and_or.smt2
+++ b/test/regress/regress3/bv_to_int_and_or.smt2
@@ -1,5 +1,7 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1  
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2  
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1   --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=1   --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2   --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=bitwise --bvand-integer-granularity=2   --no-check-unsat-cores --no-check-proofs
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 4))
diff --git a/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2
index aeacda35e..3a0320119 100644
--- a/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2
+++ b/test/regress/regress3/bv_to_int_bench_9839.smt2.minimized.smt2
@@ -1,5 +1,6 @@
-; COMMAND-LINE:  --solve-bv-as-int=bv 
-; COMMAND-LINE:  --bvand-integer-granularity=1 --solve-bv-as-int=sum     
+; COMMAND-LINE:  --solve-bv-as-int=bv
+; COMMAND-LINE:  --bvand-integer-granularity=1 --solve-bv-as-int=sum
+; COMMAND-LINE:  --bvand-integer-granularity=1 --solve-bv-as-int=bitwise
 ; EXPECT: sat
 (set-logic QF_BV)
 (declare-fun _substvar_1171_ () (_ BitVec 32))
diff --git a/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2
index c4988e3c6..3c50acc1c 100644
--- a/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2
+++ b/test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2
@@ -1,6 +1,6 @@
-; COMMAND-LINE:  --solve-bv-as-int=bv 
-; COMMAND-LINE:  --solve-bv-as-int=sum     
-; COMMAND-LINE:  --solve-bv-as-int=iand --iand-mode=sum    
+; COMMAND-LINE:  --solve-bv-as-int=bv
+; COMMAND-LINE:  --solve-bv-as-int=sum
+; COMMAND-LINE:  --solve-bv-as-int=iand --iand-mode=sum
 ; COMMAND-LINE:  --solve-bv-as-int=iand --iand-mode=bitwise
 ; COMMAND-LINE:  --solve-bv-as-int=iand --iand-mode=value
 ; EXPECT: unsat
diff --git a/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2 b/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2
index dd7e11a50..b37dc371d 100644
--- a/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2
+++ b/test/regress/regress3/bv_to_int_input_mouser_detect.c.smt2.minimized.smt2
@@ -1,5 +1,5 @@
 ; COMMAND-LINE:  --solve-bv-as-int=bv  --no-check-models
-; COMMAND-LINE:  --bvand-integer-granularity=1 --solve-bv-as-int=sum --full-saturate-quant --cegqi-all  --no-check-models  
+; COMMAND-LINE:  --bvand-integer-granularity=1 --solve-bv-as-int=sum --full-saturate-quant --cegqi-all  --no-check-models
 ;EXPECT: sat
 (set-logic BV)
 (assert (exists ((c__detect__main__1__i_36_C (_ BitVec 32))) (bvslt ((_ sign_extend 32) c__detect__main__1__i_36_C) (_ bv0 64))))
diff --git a/test/unit/theory/theory_bv_int_blaster_white.cpp b/test/unit/theory/theory_bv_int_blaster_white.cpp
index 0412fdabb..e8238ecbb 100644
--- a/test/unit/theory/theory_bv_int_blaster_white.cpp
+++ b/test/unit/theory/theory_bv_int_blaster_white.cpp
@@ -61,7 +61,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_constants)
   Env env(d_nodeManager, &opts);
   env.d_logic.setLogicString("QF_UFBV");
   env.d_logic.lock();
-  IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1, false);
+  IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1);
   Node result = intBlaster.translateNoChildren(bv7_4, lemmas, skolems);
   Node seven = d_nodeManager->mkConst(CONST_RATIONAL, Rational(7));
   ASSERT_EQ(seven, result);
@@ -86,7 +86,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_symbolic_constant)
   Env env(d_nodeManager, &opts);
   env.d_logic.setLogicString("QF_UFBV");
   env.d_logic.lock();
-  IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1, true);
+  IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1);
   Node result = intBlaster.translateNoChildren(bv, lemmas, skolems);
   ASSERT_TRUE(result.isVar() && result.getType().isInteger());
 
@@ -116,7 +116,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_uf)
   Env env(d_nodeManager, &opts);
   env.d_logic.setLogicString("QF_UFBV");
   env.d_logic.lock();
-  IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1, true);
+  IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1);
   Node result = intBlaster.translateNoChildren(f, lemmas, skolems);
   TypeNode resultType = result.getType();
   std::vector<TypeNode> resultDomain = resultType.getArgTypes();
@@ -143,7 +143,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_with_children)
   Env env(d_nodeManager, &opts);
   env.d_logic.setLogicString("QF_UFBV");
   env.d_logic.lock();
-  IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1, true);
+  IntBlaster intBlaster(env, options::SolveBVAsIntMode::SUM, 1);
 
   // bit-vector variables
   TypeNode bvType = d_nodeManager->mkBitVectorType(4);
@@ -294,7 +294,7 @@ TEST_F(TestTheoryWhiteBvIntblaster, intblaster_bitwise)
   Env env(d_nodeManager, &opts);
   env.d_logic.setLogicString("QF_UFBV");
   env.d_logic.lock();
-  IntBlaster intBlaster(env, options::SolveBVAsIntMode::BITWISE, 1, true);
+  IntBlaster intBlaster(env, options::SolveBVAsIntMode::BITWISE, 1);
 
   // bit-vector variables
   TypeNode bvType = d_nodeManager->mkBitVectorType(4);