bv_to_int preprocessing pass

Introduces a preprocessing pass that translates bv problems to integer problems.

19 files changed, 1521 insertions, 3 deletions

diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 9a81ccc63..4567f45be 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -56,6 +56,8 @@ libcvc4_add_sources(
   preprocessing/passes/bv_intro_pow2.h
   preprocessing/passes/bv_to_bool.cpp
   preprocessing/passes/bv_to_bool.h
+  preprocessing/passes/bv_to_int.cpp
+  preprocessing/passes/bv_to_int.h
   preprocessing/passes/extended_rewriter_pass.cpp
   preprocessing/passes/extended_rewriter_pass.h
   preprocessing/passes/global_negate.cpp
diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index f78dbb3b8..024530224 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -665,6 +665,15 @@ header = "options/smt_options.h"
   help       = "Force no CPU limit when dumping models and proofs"
 
 [[option]]
+  name       = "solveBVAsInt"
+  category   = "undocumented"
+  long       = "solve-bv-as-int=N"
+  type       = "uint32_t"
+  default    = "0"
+  read_only  = true
+  help       = "attempt to solve BV formulas by translation to integer arithmetic (experimental)"
+
+[[option]]
   name       = "solveIntAsBV"
   category   = "undocumented"
   long       = "solve-int-as-bv=N"
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
new file mode 100644
index 000000000..75136913c
--- /dev/null
+++ b/src/preprocessing/passes/bv_to_int.cpp
@@ -0,0 +1,977 @@
+/*********************                                                        */
+/*! \file bv_to_int.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Yoni Zohar and Ahmed Irfan
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief The BVToInt preprocessing pass
+ **
+ ** Converts bit-vector operations into integer operations.
+ **
+ **/
+
+#include "preprocessing/passes/bv_to_int.h"
+
+#include <cmath>
+#include <string>
+#include <unordered_map>
+#include <vector>
+
+#include "expr/node.h"
+#include "theory/bv/theory_bv_rewrite_rules_operator_elimination.h"
+#include "theory/bv/theory_bv_rewrite_rules_simplification.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+using namespace CVC4::theory::bv;
+
+namespace {
+
+Rational intpow2(uint64_t b)
+{
+  return Rational(Integer(2).pow(b), Integer(1));
+}
+
+/**
+ * Helper functions for createBitwiseNode
+ */
+bool oneBitAnd(bool a, bool b) { return (a && b); }
+
+bool oneBitOr(bool a, bool b) { return (a || b); }
+
+bool oneBitXor(bool a, bool b) { return a != b; }
+
+bool oneBitXnor(bool a, bool b) { return a == b; }
+
+bool oneBitNand(bool a, bool b) { return !(a && b); }
+
+bool oneBitNor(bool a, bool b) { return !(a || b); }
+
+} //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 Rewriter::rewrite(result);
+}
+
+Node BVToInt::maxInt(uint64_t k)
+{
+  Assert(k > 0);
+  Rational max_value = intpow2(k) - 1;
+  return d_nm->mkConst<Rational>(max_value);
+}
+
+Node BVToInt::pow2(uint64_t k)
+{
+  Assert(k >= 0);
+  return d_nm->mkConst<Rational>(intpow2(k));
+}
+
+Node BVToInt::modpow2(Node n, uint64_t exponent)
+{
+  Node p2 = d_nm->mkConst<Rational>(intpow2(exponent));
+  return d_nm->mkNode(kind::INTS_MODULUS_TOTAL, n, p2);
+}
+
+/**
+ * Binarizing n via post-order traversal.
+ */
+Node BVToInt::makeBinary(Node n)
+{
+  vector<Node> toVisit;
+  toVisit.push_back(n);
+  while (!toVisit.empty())
+  {
+    Node current = toVisit.back();
+    uint64_t numChildren = current.getNumChildren();
+    if (d_binarizeCache.find(current) == d_binarizeCache.end())
+    {
+      /**
+       * We still haven't visited the sub-dag rooted at the current node.
+       * In this case, we:
+       * mark that we have visited this node by assigning a null node to it in
+       * the cache, and add its children to toVisit.
+       */
+      d_binarizeCache[current] = Node();
+      toVisit.insert(toVisit.end(), current.begin(), current.end());
+    }
+    else if (d_binarizeCache[current].isNull())
+    {
+      /*
+       * We already visited the sub-dag rooted at the current node,
+       * and binarized all its children.
+       * Now we binarize the current node itself.
+       */
+      toVisit.pop_back();
+      kind::Kind_t k = current.getKind();
+      if ((numChildren > 2)
+          && (k == kind::BITVECTOR_PLUS || 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.getKind() == kind::BITVECTOR_EXTRACT
+            || current.getKind() == kind::APPLY_UF)
+        {
+          builder << current.getOperator();
+        }
+        for (Node child : current)
+        {
+          builder << d_binarizeCache[child];
+        }
+        d_binarizeCache[current] = builder.constructNode();
+      }
+      else
+      {
+        // current has no children
+        d_binarizeCache[current] = current;
+      }
+    }
+    else
+    {
+      // We already binarized current and it is in the cache.
+      toVisit.pop_back();
+    }
+  }
+  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();
+    toVisit.pop_back();
+    bool inEliminationCache =
+        (d_eliminationCache.find(current) != d_eliminationCache.end());
+    bool inRebuildCache =
+        (d_rebuildCache.find(current) != d_rebuildCache.end());
+    if (!inRebuildCache)
+    {
+      // current is not the elimination of any previously-visited node
+      if (!inEliminationCache)
+      {
+        // current hasn't been eliminated yet.
+        // eliminate operators from it
+        Node currentEliminated =
+            FixpointRewriteStrategy<RewriteRule<UdivZero>,
+                                    RewriteRule<SdivEliminate>,
+                                    RewriteRule<SremEliminate>,
+                                    RewriteRule<SmodEliminate>,
+                                    RewriteRule<RepeatEliminate>,
+                                    RewriteRule<ZeroExtendEliminate>,
+                                    RewriteRule<SignExtendEliminate>,
+                                    RewriteRule<RotateRightEliminate>,
+                                    RewriteRule<RotateLeftEliminate>,
+                                    RewriteRule<CompEliminate>,
+                                    RewriteRule<SleEliminate>,
+                                    RewriteRule<SltEliminate>,
+                                    RewriteRule<SgtEliminate>,
+                                    RewriteRule<SgeEliminate>,
+                                    RewriteRule<ShlByConst>,
+                                    RewriteRule<LshrByConst> >::apply(current);
+        // save in the cache
+        d_eliminationCache[current] = 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());
+      }
+    }
+    else
+    {
+      // current was already added to the rebuild cache.
+      if (d_rebuildCache[current].isNull())
+      {
+        // current wasn't rebuilt yet.
+        uint64_t 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.getKind() == kind::BITVECTOR_EXTRACT
+              || current.getKind() == kind::APPLY_UF)
+          {
+            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].isNull());
+            builder << d_rebuildCache[eliminatedChild];
+          }
+          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].isNull());
+  return d_rebuildCache[eliminated];
+}
+
+/**
+ * Translate n to Integers via post-order traversal.
+ */
+Node BVToInt::bvToInt(Node n)
+{
+  n = eliminationPass(n);
+  n = makeBinary(n);
+  vector<Node> toVisit;
+  toVisit.push_back(n);
+  uint64_t granularity = options::solveBVAsInt();
+
+  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.
+      d_bvToIntCache[current] = Node();
+      toVisit.insert(toVisit.end(), current.begin(), current.end());
+    }
+    else
+    {
+      // We already visited this node
+      if (!d_bvToIntCache[current].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.
+        if (currentNumChildren == 0)
+        {
+          Assert(current.isVar() || current.isConst());
+          if (current.isVar())
+          {
+            if (current.getType().isBitVector())
+            {
+              // For bit-vector variables, we create integer variables and add a
+              // range constraint.
+              Node newVar = d_nm->mkSkolem("__bvToInt_var",
+                                           d_nm->integerType(),
+                                           "Variable introduced in bvToInt "
+                                           "pass instead of original variable "
+                                               + current.toString());
+
+              d_bvToIntCache[current] = newVar;
+              d_rangeAssertions.insert(mkRangeConstraint(
+                  newVar, current.getType().getBitVectorSize()));
+            }
+            else
+            {
+              // Boolean variables are left unchanged.
+              AlwaysAssert(current.getType() == d_nm->booleanType()
+                           || current.getType().isSort());
+              d_bvToIntCache[current] = current;
+            }
+          }
+          else
+          {
+            // current is a const
+            if (current.getKind() == kind::CONST_BITVECTOR)
+            {
+              // Bit-vector constants are transformed into their integer value.
+              BitVector constant(current.getConst<BitVector>());
+              Integer c = constant.toInteger();
+              d_bvToIntCache[current] = d_nm->mkConst<Rational>(c);
+            }
+            else
+            {
+              // Other constants stay the same.
+              d_bvToIntCache[current] = 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 future use.
+           */
+          vector<Node> translated_children;
+          for (uint64_t i = 0; i < currentNumChildren; i++)
+          {
+            translated_children.push_back(d_bvToIntCache[current[i]]);
+          }
+          // The translation of the current node is determined by the kind of
+          // the node.
+          kind::Kind_t oldKind = current.getKind();
+          //ultbv and sltbv were supposed to be eliminated before this point.
+          Assert(oldKind != kind::BITVECTOR_ULTBV);
+          Assert(oldKind != kind::BITVECTOR_SLTBV);
+          switch (oldKind)
+          {
+            case kind::BITVECTOR_PLUS:
+            {
+              uint64_t bvsize = current[0].getType().getBitVectorSize();
+              /**
+               * we avoid modular arithmetics by the addition of an
+               * indicator variable sigma.
+               * Tr(a+b) is Tr(a)+Tr(b)-(sigma*2^k),
+               * with k being the bit width,
+               * and sigma being either 0 or 1.
+               */
+              Node sigma = d_nm->mkSkolem(
+                  "__bvToInt_sigma_var",
+                  d_nm->integerType(),
+                  "Variable introduced in bvToInt pass to avoid integer mod");
+              Node plus = d_nm->mkNode(kind::PLUS, translated_children);
+              Node multSig = d_nm->mkNode(kind::MULT, sigma, pow2(bvsize));
+              d_bvToIntCache[current] =
+                  d_nm->mkNode(kind::MINUS, plus, multSig);
+              d_rangeAssertions.insert(d_nm->mkNode(kind::LEQ, d_zero, sigma));
+              d_rangeAssertions.insert(d_nm->mkNode(kind::LEQ, sigma, d_one));
+              d_rangeAssertions.insert(
+                  mkRangeConstraint(d_bvToIntCache[current], bvsize));
+              break;
+            }
+            case kind::BITVECTOR_MULT:
+            {
+              uint64_t bvsize = current[0].getType().getBitVectorSize();
+              /**
+               * we use a similar trick to the one used for addition.
+               * Tr(a*b) is Tr(a)*Tr(b)-(sigma*2^k),
+               * with k being the bit width,
+               * and sigma is between [0, 2^k - 1).
+               */
+              Node sigma = d_nm->mkSkolem(
+                  "__bvToInt_sigma_var",
+                  d_nm->integerType(),
+                  "Variable introduced in bvToInt pass to avoid integer mod");
+              Node mult = d_nm->mkNode(kind::MULT, translated_children);
+              Node multSig = d_nm->mkNode(kind::MULT, sigma, pow2(bvsize));
+              d_bvToIntCache[current] =
+                  d_nm->mkNode(kind::MINUS, mult, multSig);
+              d_rangeAssertions.insert(
+                  mkRangeConstraint(d_bvToIntCache[current], bvsize));
+              d_rangeAssertions.insert(mkRangeConstraint(sigma, bvsize));
+              break;
+            }
+            case kind::BITVECTOR_UDIV_TOTAL:
+            {
+              uint64_t bvsize = current[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);
+              Node ite = d_nm->mkNode(
+                  kind::ITE,
+                  d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero),
+                  d_nm->mkNode(kind::MINUS, pow2BvSize, d_one),
+                  divNode);
+              d_bvToIntCache[current] = ite;
+              break;
+            }
+            case kind::BITVECTOR_UREM_TOTAL:
+            {
+              // we use an ITE for the case where the second operand is 0.
+              Node modNode =
+                  d_nm->mkNode(kind::INTS_MODULUS_TOTAL, translated_children);
+              Node ite = d_nm->mkNode(
+                  kind::ITE,
+                  d_nm->mkNode(kind::EQUAL, translated_children[1], d_zero),
+                  translated_children[0],
+                  modNode);
+              d_bvToIntCache[current] = ite;
+              break;
+            }
+            case kind::BITVECTOR_NEG:
+            {
+              // (bvneg x) is 2^k-x, unless x is 0, 
+              // in which case the result should be 0.
+              // This can be expressed by (2^k-x) mod 2^k
+              // However, since mod is an expensive arithmetic operation,
+              // we represent `bvneg` using an ITE.
+              uint64_t bvsize = current[0].getType().getBitVectorSize();
+              Node pow2BvSize = pow2(bvsize);
+              Node neg =
+                  d_nm->mkNode(kind::MINUS, pow2BvSize, translated_children[0]);
+              Node isZero =
+                  d_nm->mkNode(kind::EQUAL, translated_children[0], d_zero);
+              d_bvToIntCache[current] =
+                  d_nm->mkNode(kind::ITE, isZero, d_zero, neg);
+              break;
+            }
+            case kind::BITVECTOR_NOT:
+            {
+              uint64_t bvsize = current[0].getType().getBitVectorSize();
+              // we use a specified function to generate the node.
+              d_bvToIntCache[current] =
+                  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.
+              d_bvToIntCache[current] = translated_children[0];
+              break;
+            }
+            case kind::BITVECTOR_AND:
+            {
+              // Construct an ite, based on granularity.
+              uint64_t bvsize = current[0].getType().getBitVectorSize();
+              Assert(translated_children.size() == 2);
+              Node newNode = createBitwiseNode(translated_children[0],
+                                               translated_children[1],
+                                               bvsize,
+                                               granularity,
+                                               &oneBitAnd);
+              d_bvToIntCache[current] = newNode;
+              break;
+            }
+            case kind::BITVECTOR_OR:
+            {
+              // Construct an ite, based on granularity.
+              uint64_t bvsize = current[0].getType().getBitVectorSize();
+              Node newNode = createBitwiseNode(translated_children[0],
+                                               translated_children[1],
+                                               bvsize,
+                                               granularity,
+                                               &oneBitOr);
+              d_bvToIntCache[current] = newNode;
+              break;
+            }
+            case kind::BITVECTOR_XOR:
+            {
+              // Construct an ite, based on granularity.
+              uint64_t bvsize = current[0].getType().getBitVectorSize();
+              Node newNode = createBitwiseNode(translated_children[0],
+                                               translated_children[1],
+                                               bvsize,
+                                               granularity,
+                                               &oneBitXor);
+              d_bvToIntCache[current] = newNode;
+              break;
+            }
+            case kind::BITVECTOR_XNOR:
+            {
+              // Construct an ite, based on granularity.
+              uint64_t bvsize = current[0].getType().getBitVectorSize();
+              Node newNode = createBitwiseNode(translated_children[0],
+                                               translated_children[1],
+                                               bvsize,
+                                               granularity,
+                                               &oneBitXnor);
+              d_bvToIntCache[current] = newNode;
+              break;
+            }
+            case kind::BITVECTOR_NAND:
+            {
+              // Construct an ite, based on granularity.
+              uint64_t bvsize = current[0].getType().getBitVectorSize();
+              Node newNode = createBitwiseNode(translated_children[0],
+                                               translated_children[1],
+                                               bvsize,
+                                               granularity,
+                                               &oneBitNand);
+              d_bvToIntCache[current] = newNode;
+              break;
+            }
+            case kind::BITVECTOR_NOR:
+            {
+              // Construct an ite, based on granularity.
+              uint64_t bvsize = current[0].getType().getBitVectorSize();
+              Node newNode = createBitwiseNode(translated_children[0],
+                                               translated_children[1],
+                                               bvsize,
+                                               granularity,
+                                               &oneBitNor);
+              d_bvToIntCache[current] = newNode;
+              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 = current[0].getType().getBitVectorSize();
+              Node newNode = createShiftNode(translated_children, bvsize, true);
+              d_bvToIntCache[current] = newNode;
+              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 = current[0].getType().getBitVectorSize();
+              Node newNode = createShiftNode(translated_children, bvsize, false);
+              d_bvToIntCache[current] = newNode;
+              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 = current[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);
+              Node ite = d_nm->mkNode(kind::ITE, condition, thenNode, elseNode);
+              d_bvToIntCache[current] = ite;
+              break;
+            }
+            case kind::BITVECTOR_ITE:
+            {
+              // Lifted to a boolean ite.
+              Node cond = d_nm->mkNode(kind::EQUAL, translated_children[0], d_one);
+              Node ite = d_nm->mkNode(
+                  kind::ITE, cond, translated_children[1], translated_children[2]);
+              d_bvToIntCache[current] = ite;
+              break;
+            }
+            case kind::BITVECTOR_CONCAT:
+            {
+              // (concat a b) translates to a*2^k+b, k being the bitwidth of b.
+              uint64_t bvsizeRight = current[1].getType().getBitVectorSize();
+              Node pow2BvSizeRight = pow2(bvsizeRight);
+              Node a = d_nm->mkNode(
+                  kind::MULT, translated_children[0], pow2BvSizeRight);
+              Node b = translated_children[1];
+              Node sum = d_nm->mkNode(kind::PLUS, a, b);
+              d_bvToIntCache[current] = sum;
+              break;
+            }
+            case kind::BITVECTOR_EXTRACT:
+            {
+              // ((_ extract i j) a) is a / 2^j mod 2^{i-j+1}
+              // current = a[i:j]
+              Node a = current[0];
+              uint64_t i = bv::utils::getExtractHigh(current);
+              uint64_t j = bv::utils::getExtractLow(current);
+              Assert(d_bvToIntCache.find(a) != d_bvToIntCache.end());
+              Assert(i >= j);
+              Node div = d_nm->mkNode(
+                  kind::INTS_DIVISION_TOTAL, d_bvToIntCache[a], pow2(j));
+              d_bvToIntCache[current] = modpow2(div, i - j + 1);
+              break;
+            }
+            case kind::EQUAL:
+            {
+              d_bvToIntCache[current] =
+                  d_nm->mkNode(kind::EQUAL, translated_children);
+              break;
+            }
+            case kind::BITVECTOR_ULT:
+            {
+              d_bvToIntCache[current] =
+                  d_nm->mkNode(kind::LT, translated_children);
+              break;
+            }
+            case kind::BITVECTOR_ULE:
+            {
+              d_bvToIntCache[current] =
+                  d_nm->mkNode(kind::LEQ, translated_children);
+              break;
+            }
+            case kind::BITVECTOR_UGT:
+            {
+              d_bvToIntCache[current] =
+                  d_nm->mkNode(kind::GT, translated_children);
+              break;
+            }
+            case kind::BITVECTOR_UGE:
+            {
+              d_bvToIntCache[current] =
+                  d_nm->mkNode(kind::GEQ, translated_children);
+              break;
+            }
+            case kind::LT:
+            {
+              d_bvToIntCache[current] =
+                  d_nm->mkNode(kind::LT, translated_children);
+              break;
+            }
+            case kind::LEQ:
+            {
+              d_bvToIntCache[current] =
+                  d_nm->mkNode(kind::LEQ, translated_children);
+              break;
+            }
+            case kind::GT:
+            {
+              d_bvToIntCache[current] =
+                  d_nm->mkNode(kind::GT, translated_children);
+              break;
+            }
+            case kind::GEQ:
+            {
+              d_bvToIntCache[current] =
+                  d_nm->mkNode(kind::GEQ, translated_children);
+              break;
+            }
+            case kind::ITE:
+            {
+              d_bvToIntCache[current] = d_nm->mkNode(oldKind, translated_children);
+              break;
+            }
+            case kind::APPLY_UF:
+            {
+              /*
+               * We replace all BV-sorts of the domain with INT
+               * If the range is a BV sort, we replace it with INT
+               * We cache both the term itself (e.g., f(a)) and the function
+               * symbol f.
+               */
+              Node bvUF = current.getOperator();
+              Node intUF;
+              TypeNode tn = current.getOperator().getType();
+              TypeNode bvRange = tn.getRangeType();
+              if (d_bvToIntCache.find(bvUF) != d_bvToIntCache.end())
+              {
+                intUF = d_bvToIntCache[bvUF];
+              }
+              else
+              {
+                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.
+                 */
+                TypeNode intRange =
+                    bvRange.isBitVector() ? d_nm->integerType() : bvRange;
+                for (TypeNode d : bvDomain)
+                {
+                  intDomain.push_back(d.isBitVector() ? d_nm->integerType()
+                                                      : d);
+                }
+                ostringstream os;
+                os << "__bvToInt_fun_" << bvUF << "_int";
+                intUF =
+                    d_nm->mkSkolem(os.str(),
+                                   d_nm->mkFunctionType(intDomain, intRange),
+                                   "bv2int function");
+                // Insert the function symbol itself to the cache
+                d_bvToIntCache[bvUF] = intUF;
+              }
+              translated_children.insert(translated_children.begin(), intUF);
+              // Insert the term to the cache
+              d_bvToIntCache[current] =
+                  d_nm->mkNode(kind::APPLY_UF, translated_children);
+              /**
+               * Add range constraints if necessary.
+               * If the original range was a BV sort, the current application of
+               * the fucntion Must be within the range determined by the
+               * bitwidth.
+               */
+              if (bvRange.isBitVector())
+              {
+                d_rangeAssertions.insert(
+                    mkRangeConstraint(d_bvToIntCache[current],
+                                      current.getType().getBitVectorSize()));
+              }
+              break;
+            }
+            default:
+            {
+              if (Theory::theoryOf(current) == THEORY_BOOL)
+              {
+                d_bvToIntCache[current] =
+                    d_nm->mkNode(oldKind, translated_children);
+                break;
+              }
+              else
+              {
+                // Currently, only QF_UFBV formulas are handled.
+                // In the future, more theories should be supported, e.g., arrays.
+                Unimplemented();
+              }
+            }
+          }
+        }
+        toVisit.pop_back();
+      }
+    }
+  }
+  return d_bvToIntCache[n];
+}
+
+BVToInt::BVToInt(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "bv-to-int"),
+      d_binarizeCache(),
+      d_eliminationCache(),
+      d_bvToIntCache(),
+      d_rangeAssertions()
+{
+  d_nm = NodeManager::currentNM();
+  d_zero = d_nm->mkConst<Rational>(0);
+  d_one = d_nm->mkConst<Rational>(1);
+};
+
+PreprocessingPassResult BVToInt::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  AlwaysAssert(!options::incrementalSolving());
+  for (uint64_t i = 0; i < assertionsToPreprocess->size(); ++i)
+  {
+    Node bvNode = (*assertionsToPreprocess)[i];
+    Node intNode = bvToInt(bvNode);
+    Node rwNode = Rewriter::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);
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+void BVToInt::addFinalizeRangeAssertions(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  vector<Node> vec_range;
+  vec_range.assign(d_rangeAssertions.begin(), d_rangeAssertions.end());
+  if (vec_range.size() == 1)
+  {
+    assertionsToPreprocess->push_back(vec_range[0]);
+    Trace("bv-to-int-debug")
+        << "range constraints: " << vec_range[0].toString() << std::endl;
+  }
+  else if (vec_range.size() >= 2)
+  {
+    Node rangeAssertions =
+        Rewriter::rewrite(d_nm->mkNode(kind::AND, 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)
+{
+  Node x = children[0];
+  Node y = children[1];
+  Assert(!y.isConst());
+  // ite represents 2^x for every integer x from 0 to bvsize-1.
+  Node ite = pow2(0);
+  for (uint64_t i = 1; i < bvsize; i++)
+  {
+    ite = d_nm->mkNode(kind::ITE,
+                       d_nm->mkNode(kind::EQUAL, y, d_nm->mkConst<Rational>(i)),
+                       pow2(i),
+                       ite);
+  }
+  /**
+   * 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 the ite declared above.
+   */
+  kind::Kind_t then_kind = isLeftShift ? kind::MULT : kind::INTS_DIVISION_TOTAL;
+  return d_nm->mkNode(kind::ITE,
+                              d_nm->mkNode(kind::LT, y, d_nm->mkConst<Rational>(bvsize)),
+                              d_nm->mkNode(kind::INTS_MODULUS_TOTAL,
+                                                            d_nm->mkNode(then_kind, x, ite),
+                                                            pow2(bvsize)),
+                              d_zero);
+}
+
+Node BVToInt::createITEFromTable(
+    Node x,
+    Node y,
+    uint64_t granularity,
+    std::map<std::pair<uint64_t, uint64_t>, uint64_t> table)
+{
+  Assert(granularity <= 8);
+  uint64_t max_value = ((uint64_t)pow(2, granularity));
+  // The table represents a function from pairs of integers to integers, where
+  // all integers are between 0 (inclusive) and max_value (exclusive).
+  Assert(table.size() == max_value * max_value);
+  Node ite = d_nm->mkConst<Rational>(table[std::make_pair(0, 0)]);
+  for (uint64_t i = 0; i < max_value; i++)
+  {
+    for (uint64_t j = 0; j < max_value; j++)
+    {
+      if ((i == 0) && (j == 0))
+      {
+        continue;
+      }
+      ite = d_nm->mkNode(
+          kind::ITE,
+          d_nm->mkNode(
+              kind::AND,
+              d_nm->mkNode(kind::EQUAL, x, d_nm->mkConst<Rational>(i)),
+              d_nm->mkNode(kind::EQUAL, y, d_nm->mkConst<Rational>(j))),
+          d_nm->mkConst<Rational>(table[std::make_pair(i, j)]),
+          ite);
+    }
+  }
+  return ite;
+}
+
+Node BVToInt::createBitwiseNode(Node x,
+                                Node y,
+                                uint64_t bvsize,
+                                uint64_t granularity,
+                                bool (*f)(bool, bool))
+{
+  /**
+   * Standardize granularity.
+   * If it is greater than bvsize, it is set to bvsize.
+   * Otherwise, it is set to the closest (going down)  divider of bvsize.
+   */
+  Assert(granularity > 0);
+  if (granularity > bvsize)
+  {
+    granularity = bvsize;
+  }
+  else
+  {
+    while (bvsize % granularity != 0)
+    {
+      granularity = granularity - 1;
+    }
+  }
+  // transform f into a table
+  // f is defined over 1 bit, while the table is defined over `granularity` bits
+  std::map<std::pair<uint64_t, uint64_t>, uint64_t> table;
+  uint64_t max_value = ((uint64_t)pow(2, granularity));
+  for (uint64_t i = 0; i < max_value; i++)
+  {
+    for (uint64_t j = 0; j < max_value; j++)
+    {
+      uint64_t sum = 0;
+      for (uint64_t n = 0; n < granularity; n++)
+      {
+        // b is the result of f on the current bit
+        bool b = f((((i >> n) & 1) == 1), (((j >> n) & 1) == 1));
+        // add the corresponding power of 2 only if the result is 1
+        if (b)
+        {
+          sum += 1 << n;
+        }
+      }
+      table[std::make_pair(i, j)] = sum;
+    }
+  }
+   Assert(table.size() == max_value * max_value);
+
+  /*
+   * Create the sum.
+   * For granularity 1, the sum has bvsize elements.
+   * In contrast, if bvsize = granularity, sum has one element.
+   * Each element in the sum is an ite that corresponds to the generated table,
+   * multiplied by the appropriate power of two.
+   * More details are in bv_to_int.h .
+   */
+  uint64_t sumSize = bvsize / granularity;
+  Node sumNode = d_zero;
+  /**
+   * extract definition in integers is:
+   * (define-fun intextract ((k Int) (i Int) (j Int) (a Int)) Int
+   * (mod (div a (two_to_the j)) (two_to_the (+ (- i j) 1))))
+   */
+  for (uint64_t i = 0; i < sumSize; i++)
+  {
+    Node xExtract = d_nm->mkNode(
+        kind::INTS_MODULUS_TOTAL,
+        d_nm->mkNode(kind::INTS_DIVISION_TOTAL, x, pow2(i * granularity)),
+        pow2(granularity));
+    Node yExtract = d_nm->mkNode(
+        kind::INTS_MODULUS_TOTAL,
+        d_nm->mkNode(kind::INTS_DIVISION_TOTAL, y, pow2(i * granularity)),
+        pow2(granularity));
+    Node ite = createITEFromTable(xExtract, yExtract, granularity, table);
+    sumNode =
+        d_nm->mkNode(kind::PLUS,
+                     sumNode,
+                     d_nm->mkNode(kind::MULT, pow2(i * granularity), ite));
+  }
+  return sumNode;
+}
+
+Node BVToInt::createBVNotNode(Node n, uint64_t bvsize)
+{
+  return d_nm->mkNode(kind::MINUS, maxInt(bvsize), n);
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/preprocessing/passes/bv_to_int.h b/src/preprocessing/passes/bv_to_int.h
new file mode 100644
index 000000000..dd02d98ec
--- /dev/null
+++ b/src/preprocessing/passes/bv_to_int.h
@@ -0,0 +1,273 @@
+/*********************                                                        */
+/*! \file bv_to_int.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Yoni Zohar and Ahmed Irfan
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 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.\endverbatim
+ **
+ ** \brief 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((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)
+ **
+ ** More details and examples for this case are described next to
+ ** the function createBitwiseNode.
+ ** 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.
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
+#define __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using NodeMap = std::unordered_map<Node, Node, NodeHashFunction>;
+
+class BVToInt : public PreprocessingPass
+{
+ public:
+  BVToInt(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+
+  /**
+   * A generic function that creates a node that represents a bitwise
+   * operation.
+   *
+   * For example: Suppose bvsize is 4, granularity is 1, and f(x,y) = x && y.
+   * Denote by ITE(a,b) the term: ite(a==0, 0, ite(b==1, 1, 0)).
+   * The result of this function would be:
+   * ITE(x[0], y[0])*2^0 + ... + ITE(x[3], y[3])*2^3
+   *
+   * For another example: Suppose bvsize is 4, granularity is 2,
+   * and f(x,y) = x && y.
+   * Denote by ITE(a,b) the term that corresponds to the following table:
+   * a | b |  ITE(a,b)
+   * ----------------
+   * 0 | 0 | 0
+   * 0 | 1 | 0
+   * 0 | 2 | 0
+   * 0 | 3 | 0
+   * 1 | 0 | 0
+   * 1 | 1 | 1
+   * 1 | 2 | 0
+   * 1 | 3 | 1
+   * 2 | 0 | 0
+   * 2 | 1 | 0
+   * 2 | 2 | 2
+   * 2 | 3 | 2
+   * 3 | 0 | 0
+   * 3 | 1 | 1
+   * 3 | 2 | 2
+   * 3 | 3 | 3
+   *
+   * For example, 2 in binary is 10 and 1 in binary is 01, and so doing
+   * "bitwise f" on them gives 00.
+   * The result of this function would be:
+   * ITE(x[1:0], y[1:0])*2^0 + ITE(x[3:2], y[3:2])*2^2
+   *
+   *
+   * @param x is an integer operand that correspond to the first original
+   *        bit-vector operand.
+   * @param y is an integer operand that correspond to the second original
+   *        bit-vector operand.
+   * @param bvsize is the bit width of the original bit-vector variables.
+   * @param granularity is specified in the options for this preprocessing
+   *        pass.
+   * @param f is a pointer to a boolean function that corresponds
+   *        to the original bitwise operation.
+   * @return A node that represents the operation, as described above.
+   */
+  Node createBitwiseNode(Node x,
+                         Node y,
+                         uint64_t bvsize,
+                         uint64_t granularity,
+                         bool (*f)(bool, bool));
+
+  /**
+   * A helper function for createBitwiseNode
+   * @param x integer node corresponding to the original first bit-vector
+   *        argument
+   * @param y integer node corresponding to the original second bit-vector
+   *        argument nodes.
+   * @param granularity the bitwidth of the original bit-vector nodes.
+   * @param table a function from pairs of integers to integers.
+   *        The domain of this function consists of pairs of
+   *        integers between 0 (inclusive) and 2^{bitwidth} (exclusive).
+   * @return An ite term that represents this table.
+   */
+  Node createITEFromTable(
+      Node x,
+      Node y,
+      uint64_t granularity,
+      std::map<std::pair<uint64_t, uint64_t>, uint64_t> table);
+
+  /**
+   * 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(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);
+
+  /**
+   * 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);
+
+  /**
+   * Caches for the different functions
+   */
+  NodeMap d_binarizeCache;
+  NodeMap d_eliminationCache;
+  NodeMap d_rebuildCache;
+  NodeMap d_bvToIntCache;
+
+  /**
+   * Node manager that is used throughout the pass
+   */
+  NodeManager* d_nm;
+
+  /**
+   * A set of constraints of the form 0 <= x < 2^k
+   * These are added for every new integer variable that we introduce.
+   */
+  unordered_set<Node, NodeHashFunction> d_rangeAssertions;
+
+  /**
+   * Useful constants
+   */
+  Node d_zero;
+  Node d_one;
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__BV_TO_INT_H */
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp
index 5df449237..154ed9086 100644
--- a/src/preprocessing/preprocessing_pass_registry.cpp
+++ b/src/preprocessing/preprocessing_pass_registry.cpp
@@ -32,6 +32,7 @@
 #include "preprocessing/passes/bv_gauss.h"
 #include "preprocessing/passes/bv_intro_pow2.h"
 #include "preprocessing/passes/bv_to_bool.h"
+#include "preprocessing/passes/bv_to_int.h"
 #include "preprocessing/passes/extended_rewriter_pass.h"
 #include "preprocessing/passes/global_negate.h"
 #include "preprocessing/passes/ho_elim.h"
@@ -124,6 +125,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry()
   registerPassInfo("apply-to-const", callCtor<ApplyToConst>);
   registerPassInfo("global-negate", callCtor<GlobalNegate>);
   registerPassInfo("int-to-bv", callCtor<IntToBV>);
+  registerPassInfo("bv-to-int", callCtor<BVToInt>);
   registerPassInfo("synth-rr", callCtor<SynthRewRulesPass>);
   registerPassInfo("real-to-int", callCtor<RealToInt>);
   registerPassInfo("sygus-infer", callCtor<SygusInference>);
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6f40d815f..2bfb8353f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1215,9 +1215,17 @@ void SmtEngine::setDefaults() {
     }
     d_logic = LogicInfo("QF_BV");
   }
-  else if (d_logic.getLogicString() == "QF_NRA" && options::solveRealAsInt())
+
+  if (options::solveBVAsInt() > 0)
   {
-    d_logic = LogicInfo("QF_NIA");
+    if (d_logic.isTheoryEnabled(THEORY_BV))
+    {
+      d_logic = d_logic.getUnlockedCopy();
+      d_logic.disableTheory(THEORY_BV);
+      d_logic.enableTheory(THEORY_ARITH);
+      d_logic.arithNonLinear();
+      d_logic.lock();
+    }
   }
 
   // set options about ackermannization
@@ -1441,6 +1449,17 @@ void SmtEngine::setDefaults() {
       options::preSkolemQuant.set(false);
     }
 
+    if (options::solveBVAsInt() > 0)
+    {
+      /**
+       * Operations on 1 bits are better handled as Boolean operations
+       * than as integer operations.
+       * Therefore, we enable bv-to-bool, which runs before
+       * the translation to integers.
+       */
+      options::bitvectorToBool.set(true);
+    }
+
     if (options::bitvectorToBool())
     {
       if (options::bitvectorToBool.wasSetByUser())
@@ -3297,7 +3316,7 @@ void SmtEnginePrivate::processAssertions() {
   if (options::solveRealAsInt()) {
     d_passes["real-to-int"]->apply(&d_assertions);
   }
-
+  
   if (options::solveIntAsBV() > 0)
   {
     d_passes["int-to-bv"]->apply(&d_assertions);
@@ -3358,6 +3377,34 @@ void SmtEnginePrivate::processAssertions() {
   {
     d_passes["bv-to-bool"]->apply(&d_assertions);
   }
+  if (options::solveBVAsInt() > 0)
+  {
+    if (options::incrementalSolving())
+    {
+      throw ModalException(
+          "solving bitvectors as integers is currently not supported "
+          "when solving incrementally.");
+    } else if (options::boolToBitvector() != options::BoolToBVMode::OFF) {
+      throw ModalException(
+          "solving bitvectors as integers is incompatible with --bool-to-bv.");
+    }
+    else if (options::solveBVAsInt() > 8)
+    {
+      /**
+       * The granularity sets the size of the ITE in each element
+       * of the sum that is generated for bitwise operators.
+       * The size of the ITE is 2^{2*granularity}.
+       * Since we don't want to introduce ITEs with unbounded size,
+       * we bound the granularity.
+       */
+      throw ModalException("solve-bv-as-int accepts values from 0 to 8.");
+    }
+    else
+    {
+      d_passes["bv-to-int"]->apply(&d_assertions);
+    }
+  }
+
   // Convert non-top-level Booleans to bit-vectors of size 1
   if (options::boolToBitvector() != options::BoolToBVMode::OFF)
   {
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 92a6200ee..b909817df 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -204,6 +204,15 @@ set(regress_0_tests
   regress0/bv/bv-options4.smt2
   regress0/bv/bv-to-bool1.smtv1.smt2
   regress0/bv/bv-to-bool2.smt2
+  regress0/bv/bv_to_int1.smt2
+  regress0/bv/bv_to_int2.smt2
+  regress0/bv/bv_to_int_bvmul1.smt2
+  regress0/bv/bv_to_int_bvmul2.smt2
+  regress0/bv/bv_to_int_zext.smt2
+  regress0/bv/bv_to_int_bitwise.smt2
+  regress0/bv/bvuf_to_intuf.smt2
+  regress0/bv/bvuf_to_intuf_smtlib.smt2
+  regress0/bv/bvuf_to_intuf_sorts.smt2
   regress0/bv/bv2nat-ground-c.smt2
   regress0/bv/bv2nat-simp-range.smt2
   regress0/bv/bvmul-pow2-only.smt2
@@ -1922,6 +1931,8 @@ set(regress_2_tests
   regress2/bug674.smt2
   regress2/bug765.smt2
   regress2/bug812.smt2
+  regress2/bv_to_int_ashr.smt2
+  regress2/bv_to_int_shifts.smt2
   regress2/error0.smt2
   regress2/error1.smtv1.smt2
   regress2/friedman_n4_i5.smtv1.smt2
@@ -2007,6 +2018,7 @@ set(regress_3_tests
   regress3/bmc-ibm-2.smtv1.smt2
   regress3/bmc-ibm-5.smtv1.smt2
   regress3/bmc-ibm-7.smtv1.smt2
+  regress3/bv_to_int_and_or.smt2
   regress3/eq_diamond14.smtv1.smt2
   regress3/friedman_n6_i4.smtv1.smt2
   regress3/hole9.cvc
diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2
new file mode 100644
index 000000000..1df9ec2d6
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int1.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; COMMAND-LINE: --solve-bv-as-int=2 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=3 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=4 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun x () (_ BitVec 4))
+(declare-fun y () (_ BitVec 4))
+(assert (= x (_ bv3 4)))
+(assert (= y (_ bv3 4)))
+(assert (not (bvsle (bvadd x y) (_ bv6 4))))
+(assert (= (bvadd x y) (_ bv6 4)))
+(check-sat)
diff --git a/test/regress/regress0/bv/bv_to_int2.smt2 b/test/regress/regress0/bv/bv_to_int2.smt2
new file mode 100644
index 000000000..ab1bf10f3
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int2.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=5 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models  --no-check-unsat-cores
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(assert (bvult (bvshl a b) (bvlshr a b)))
+
+(check-sat)
diff --git a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 b/test/regress/regress0/bv/bv_to_int_bitwise.smt2
new file mode 100644
index 000000000..52eb78830
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_bitwise.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=5 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun s () (_ BitVec 4))
+(declare-fun t () (_ BitVec 4))
+(assert (not (= (bvlshr s (bvor (bvand t #b0000) s)) #b0000)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul1.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
new file mode 100644
index 000000000..d0d699b4d
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_bvmul1.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=4 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models  --no-check-unsat-cores
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(assert (bvult (bvmul a b) (bvudiv a b)))
+
+(check-sat)
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
new file mode 100644
index 000000000..541229813
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun T4_180 () (_ BitVec 32))
+(assert (and 
+(= (bvmul T4_180 (_ bv1056 32)) (_ bv0 32)) 
+(not (= (bvmul T4_180 (_ bv1408 32)) (_ bv0 32))) 
+)
+)
+(check-sat)
diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2
new file mode 100644
index 000000000..3525cebb6
--- /dev/null
+++ b/test/regress/regress0/bv/bv_to_int_zext.smt2
@@ -0,0 +1,7 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun T1_31078 () (_ BitVec 8))
+(assert (let ((?v_0 ((_ zero_extend 8) T1_31078))) (and true (= ?v_0 (_ bv123 16)) (not (= (_ bv123 16) ?v_0)))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/bvuf_to_intuf.smt2 b/test/regress/regress0/bv/bvuf_to_intuf.smt2
new file mode 100644
index 000000000..7176f4012
--- /dev/null
+++ b/test/regress/regress0/bv/bvuf_to_intuf.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; EXPECT: sat
+(set-logic QF_UFBV)
+(declare-fun a () (_ BitVec 4))
+(declare-fun b () (_ BitVec 4))
+(declare-fun f ((_ BitVec 4)) (_ BitVec 4) )
+(assert (distinct (bvadd a b) (f a)))
+(check-sat)
diff --git a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
new file mode 100644
index 000000000..297bb2422
--- /dev/null
+++ b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
@@ -0,0 +1,81 @@
+;COMMAND-LINE: --solve-bv-as-int=1 --no-produce-models --no-produce-unsat-cores --no-check-proofs
+;EXPECT: unsat
+
+(set-logic QF_UFBV)
+(declare-fun z$n0s32 () (_ BitVec 32))
+(declare-fun dataOut () (_ BitVec 32))
+(declare-fun z$2 () (_ BitVec 1))
+(declare-fun stageOne () (_ BitVec 32))
+(declare-fun z$4 () (_ BitVec 1))
+(declare-fun stageTwo () (_ BitVec 32))
+(declare-fun z$6 () (_ BitVec 1))
+(declare-fun tmp_stageOne () (_ BitVec 32))
+(declare-fun z$8 () (_ BitVec 1))
+(declare-fun tmp_stageTwo () (_ BitVec 32))
+(declare-fun z$10 () (_ BitVec 1))
+(declare-fun reset_ () (_ BitVec 1))
+(declare-fun z$14 () (_ BitVec 1))
+(declare-fun Add_32_32_32 ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
+(declare-fun z$15 () (_ BitVec 32))
+(declare-fun z$17 () (_ BitVec 32))
+(declare-fun dataOut$next () (_ BitVec 32))
+(declare-fun z$19 () (_ BitVec 1))
+(declare-fun c1 () (_ BitVec 32))
+(declare-fun dataIn () (_ BitVec 32))
+(declare-fun z$23 () (_ BitVec 32))
+(declare-fun stageOne$next () (_ BitVec 32))
+(declare-fun z$25 () (_ BitVec 1))
+(declare-fun c2 () (_ BitVec 32))
+(declare-fun z$28 () (_ BitVec 32))
+(declare-fun stageTwo$next () (_ BitVec 32))
+(declare-fun z$30 () (_ BitVec 1))
+(declare-fun tmp_stageOne$next () (_ BitVec 32))
+(declare-fun z$32 () (_ BitVec 1))
+(declare-fun tmp_stageTwo$next () (_ BitVec 32))
+(declare-fun z$34 () (_ BitVec 1))
+(declare-fun z$35 () (_ BitVec 1))
+(declare-fun z$55 () (_ BitVec 32))
+(declare-fun z$57 () (_ BitVec 1))
+(declare-fun z$58 () (_ BitVec 1))
+(declare-fun z$59 () (_ BitVec 1))
+(declare-fun prop$next () (_ BitVec 1))
+(declare-fun z$61 () (_ BitVec 1))
+(declare-fun z$54 () (_ BitVec 1))
+(declare-fun z$63 () (_ BitVec 1))
+(assert
+ (= z$15 (Add_32_32_32 stageTwo stageOne)))
+(assert
+ (= z$17 (ite (= z$14 (_ bv1 1)) z$15 z$n0s32)))
+(assert
+ (= z$19 (ite (= dataOut$next z$17) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$25 (ite (= stageOne$next z$23) (_ bv1 1) (_ bv0 1))))
+
+ 
+(assert
+ (= z$32 (ite (= tmp_stageOne$next stageOne) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$34 (ite (= tmp_stageTwo$next stageTwo) (_ bv1 1) (_ bv0 1))))
+(assert
+ (let (($x130 (and (= z$19 (_ bv1 1)) (= z$25 (_ bv1 1)) (= z$30 (_ bv1 1)) (= z$32 (_ bv1 1)) (= z$34 (_ bv1 1)))))
+ (= z$35 (ite $x130 (_ bv1 1) (_ bv0 1)))))
+(assert
+ (= z$55 (Add_32_32_32 tmp_stageTwo$next tmp_stageOne$next)))
+(assert
+ (= z$57 (ite (= dataOut$next z$55) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$58 (ite (= dataOut$next z$n0s32) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$59 (ite (or (= z$57 (_ bv1 1)) (= z$58 (_ bv1 1))) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$61 (ite (= prop$next z$59) (_ bv1 1) (_ bv0 1))))
+(assert
+ (= z$54 (ite (= prop$next (_ bv0 1)) (_ bv1 1) (_ bv0 1))))
+(assert
+ (let (($x52 (= z$2 (_ bv1 1))))
+ (let (($x165 (and $x52 (= z$4 (_ bv1 1)) (= z$6 (_ bv1 1)) (= z$8 (_ bv1 1)) (= z$10 (_ bv1 1)) (= z$35 (_ bv1 1)) (= z$61 (_ bv1 1)) (= z$54 (_ bv1 1)))))
+ (= z$63 (ite $x165 (_ bv1 1) (_ bv0 1))))))
+(assert
+ (= z$63 (_ bv1 1)))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2
new file mode 100644
index 000000000..873acd6c4
--- /dev/null
+++ b/test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; EXPECT: sat
+(set-logic QF_UFBV)
+(declare-sort S 0)
+(declare-fun s () S)
+(declare-fun a () (_ BitVec 4))
+(declare-fun b () (_ BitVec 4))
+(declare-fun f ((_ BitVec 4)) (_ BitVec 4) )
+(declare-fun g (S) (_ BitVec 4))
+(declare-fun h ((_ BitVec 4)) S)
+(assert (distinct (bvadd a b) (f a)))
+(assert (distinct (f a) (g s)))
+(assert (distinct (h a) s))
+(check-sat)
diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2
new file mode 100644
index 000000000..e3fcb1790
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_ashr.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; COMMAND-LINE: --solve-bv-as-int=8 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(assert (bvult (bvashr a b) (bvlshr a b)))
+
+(check-sat)
diff --git a/test/regress/regress2/bv_to_int_shifts.smt2 b/test/regress/regress2/bv_to_int_shifts.smt2
new file mode 100644
index 000000000..39dace123
--- /dev/null
+++ b/test/regress/regress2/bv_to_int_shifts.smt2
@@ -0,0 +1,17 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores
+; EXPECT: sat
+(set-logic QF_BV)
+(declare-fun s () (_ BitVec 64))
+(declare-fun t () (_ BitVec 64))
+(declare-fun splust () (_ BitVec 64))
+(declare-fun shift1 () (_ BitVec 64))
+(declare-fun shift2 () (_ BitVec 64))
+(declare-fun negshift1 () (_ BitVec 64))
+
+(assert (= shift1 (bvlshr s splust)))
+(assert (= shift2 (bvlshr t splust)))
+(assert (= negshift1 (bvneg shift1)))
+(assert (= splust (bvadd s t)))
+(assert (distinct negshift1 shift2))
+
+(check-sat)
diff --git a/test/regress/regress3/bv_to_int_and_or.smt2 b/test/regress/regress3/bv_to_int_and_or.smt2
new file mode 100644
index 000000000..54a491093
--- /dev/null
+++ b/test/regress/regress3/bv_to_int_and_or.smt2
@@ -0,0 +1,8 @@
+; COMMAND-LINE: --solve-bv-as-int=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
+; COMMAND-LINE: --solve-bv-as-int=2 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; EXPECT: unsat
+(set-logic QF_BV)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(assert (bvult (bvor a b) (bvand a b)))
+(check-sat)