diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index c11533467f95df031d7d0dbba542cd79f51f5c86..c5bcb8d9c49ddaccf6ad845a4cc32155ea4ca722 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -33,6 +33,7 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog
     "  -P:funcheck:testbounds=l:u     Lower and upper bounds for integers in recursive datatypes" + "\n" +
     "  -P:funcheck:timeout=N          Sets a timeout of N seconds" + "\n" +
     "  -P:funcheck:XP                 Enable weird transformations and other bug-producing features" + "\n" +
+    "  -P:funcheck:BV                 Use bit-vectors for integers" + "\n" +
     "  -P:funcheck:prune              Use additional SMT queries to rule out some unrollings" + "\n" +
     "  -P:funcheck:cores              Use UNSAT cores in the unrolling/refinement step" + "\n" +
     "  -P:funcheck:quickcheck         Use QuickCheck-like random search in parrallel with Z3" + "\n" +
@@ -53,8 +54,9 @@ class FunCheckPlugin(val global: Global, val actionAfterExtraction : Option[Prog
         case "bapa"       =>                     purescala.Settings.useBAPA = true
         case "impure"     =>                     purescala.Settings.impureTestcases = true
         case "XP"         =>                     purescala.Settings.experimental = true
-        case "prune"     =>                      purescala.Settings.pruneBranches = true
-        case "cores"     =>                      purescala.Settings.useCores = true
+        case "BV"         =>                     purescala.Settings.bitvectorBitwidth = Some(32)
+        case "prune"      =>                     purescala.Settings.pruneBranches = true
+        case "cores"      =>                     purescala.Settings.useCores = true
         case "quickcheck" =>                     purescala.Settings.useQuickCheck = true
         case "noLuckyTests" =>                   purescala.Settings.luckyTest = false
         case s if s.startsWith("unrolling=") =>  purescala.Settings.unrollingLevel = try { s.substring("unrolling=".length, s.length).toInt } catch { case _ => 0 }
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 28e78b83718e5119fdac9fc851511c0a3f69a14f..e3a4002aec895b795ea5488973e2179f8b692930 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -15,6 +15,8 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
   // assert(Settings.useFairInstantiator)
 
   private final val UNKNOWNASSAT : Boolean = !Settings.noForallAxioms
+  private final val USEBV : Boolean = Settings.bitvectorBitwidth.isDefined
+  private final val BVWIDTH : Int = Settings.bitvectorBitwidth.getOrElse(-1)
 
   val description = "Fair Z3 Solver"
   override val shortDescription = "Z3-f"
@@ -121,7 +123,11 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
     case Some(z3sort) => z3sort
     case None => {
       import Z3Context.{ADTSortReference, RecursiveType, RegularSort}
-      intSort = z3.mkIntSort
+      intSort = if(USEBV) {
+        z3.mkBVSort(BVWIDTH) 
+      } else {
+        z3.mkIntSort
+      }
       boolSort = z3.mkBoolSort
 
       def typeToSortRef(tt: TypeTree): ADTSortReference = tt match {
@@ -163,7 +169,11 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
     import Z3Context.{ADTSortReference, RecursiveType, RegularSort}
     // NOTE THAT abstract classes that extend abstract classes are not
     // currently supported in the translation
-    intSort = z3.mkIntSort
+    intSort = if(USEBV) {
+      z3.mkBVSort(BVWIDTH) 
+    } else {
+      z3.mkIntSort
+    }
     boolSort = z3.mkBoolSort
     setSorts = Map.empty
     setCardFuns = Map.empty
@@ -349,7 +359,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
       case None => {
         val newSetSort = z3.mkSetSort(typeToSort(base))
         setSorts = setSorts + (base -> newSetSort)
-        val newCardFun = z3.mkFreshFuncDecl("card", Seq(newSetSort), z3.mkIntSort)
+        val newCardFun = z3.mkFreshFuncDecl("card", Seq(newSetSort), intSort)
         setCardFuns = setCardFuns + (base -> newCardFun)
         newSetSort
       }
@@ -859,15 +869,15 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
         case IntLiteral(v) => z3.mkInt(v, intSort)
         case BooleanLiteral(v) => if (v) z3.mkTrue() else z3.mkFalse()
         case Equals(l, r) => z3.mkEq(rec(l), rec(r))
-        case Plus(l, r) => z3.mkAdd(rec(l), rec(r))
-        case Minus(l, r) => z3.mkSub(rec(l), rec(r))
-        case Times(l, r) => z3.mkMul(rec(l), rec(r))
-        case Division(l, r) => z3.mkDiv(rec(l), rec(r))
-        case UMinus(e) => z3.mkUnaryMinus(rec(e))
-        case LessThan(l, r) => z3.mkLT(rec(l), rec(r))
-        case LessEquals(l, r) => z3.mkLE(rec(l), rec(r))
-        case GreaterThan(l, r) => z3.mkGT(rec(l), rec(r))
-        case GreaterEquals(l, r) => z3.mkGE(rec(l), rec(r))
+        case Plus(l, r) => if(USEBV) z3.mkBVAdd(rec(l), rec(r)) else z3.mkAdd(rec(l), rec(r))
+        case Minus(l, r) => if(USEBV) z3.mkBVSub(rec(l), rec(r)) else z3.mkSub(rec(l), rec(r))
+        case Times(l, r) => if(USEBV) z3.mkBVMul(rec(l), rec(r)) else z3.mkMul(rec(l), rec(r))
+        case Division(l, r) => if(USEBV) z3.mkBVSdiv(rec(l), rec(r)) else z3.mkDiv(rec(l), rec(r))
+        case UMinus(e) => if(USEBV) z3.mkBVNeg(rec(e)) else z3.mkUnaryMinus(rec(e))
+        case LessThan(l, r) => if(USEBV) z3.mkBVSlt(rec(l), rec(r)) else z3.mkLT(rec(l), rec(r))
+        case LessEquals(l, r) => if(USEBV) z3.mkBVSle(rec(l), rec(r)) else z3.mkLE(rec(l), rec(r))
+        case GreaterThan(l, r) => if(USEBV) z3.mkBVSgt(rec(l), rec(r)) else z3.mkGT(rec(l), rec(r))
+        case GreaterEquals(l, r) => if(USEBV) z3.mkBVSge(rec(l), rec(r)) else z3.mkGE(rec(l), rec(r))
         case c@CaseClass(cd, args) => {
           val constructor = adtConstructors(cd)
           constructor(args.map(rec(_)): _*)
diff --git a/src/purescala/Settings.scala b/src/purescala/Settings.scala
index b369a6387d4fa5c10be472877ef940be502ac53c..651a13c269cd0277c952cdd27cd6bcdf8995252e 100644
--- a/src/purescala/Settings.scala
+++ b/src/purescala/Settings.scala
@@ -23,4 +23,6 @@ object Settings {
   var solverTimeout : Option[Int] = None
   var luckyTest : Boolean = true
   var useQuickCheck : Boolean = false
+  // When this is None, use real integers
+  var bitvectorBitwidth : Option[Int] = None
 }