diff --git a/heapster-saw/examples/arrays.bc b/heapster-saw/examples/arrays.bc
index 52ffa9c5ea..99b83c8c5e 100644
Binary files a/heapster-saw/examples/arrays.bc and b/heapster-saw/examples/arrays.bc differ
diff --git a/heapster-saw/examples/arrays.c b/heapster-saw/examples/arrays.c
index da3bb6d47c..ceabdf0267 100644
--- a/heapster-saw/examples/arrays.c
+++ b/heapster-saw/examples/arrays.c
@@ -102,3 +102,23 @@ uint64_t sum_inc_ptr(const uint8_t *arr, size_t len) {
   }
   return sum;
 }
+
+/* Like the above, but uses an array of int64_t */
+uint64_t sum_inc_ptr_64(const uint64_t *arr, size_t len) {
+  uint64_t sum = 0;
+  while (len--) {
+    sum += arr[0];
+    arr += 8;
+  }
+  return sum;
+}
+
+/* For an array of even length, returns the sum of the even components of the
+   array minus the sum of the odd components of an array */
+uint64_t even_odd_sums_diff(const uint64_t *arr, size_t len) {
+  uint64_t sum = 0;
+  for (uint64_t i = 1; i < len; i += 2) {
+    sum += arr[i-1] - arr[i];
+  }
+  return sum;
+}
diff --git a/heapster-saw/examples/arrays.saw b/heapster-saw/examples/arrays.saw
index 468fbeb1a8..ee86907ea8 100644
--- a/heapster-saw/examples/arrays.saw
+++ b/heapster-saw/examples/arrays.saw
@@ -51,4 +51,15 @@ heapster_typecheck_fun env "sum_inc_ptr"
   "(len:bv 64). arg0:array(W,0,<len,*1,fieldsh(8,int8<>)), arg1:eq(llvmword(len)) -o \
               \ arg0:array(W,0,<len,*1,fieldsh(8,int8<>)), arg1:true, ret:int64<>";
 
+heapster_typecheck_fun env "sum_inc_ptr_64"
+  "(len:bv 64). arg0:array(W,0,<len,*8,fieldsh(int64<>)), arg1:eq(llvmword(len)) -o \
+              \ arg0:array(W,0,<len,*8,fieldsh(int64<>)), arg1:true, ret:int64<>";
+
+// Notably, this works even without heapster widening the permissions of `i` to
+//  `eq(2*x+1)` for some ghost `x` (currently, it sees `eq(1)` and `eq(3)` and
+//  widens them to just `eq(x)` for some ghost `x`)
+heapster_typecheck_fun env "even_odd_sums_diff"
+  "(l:bv 64). arg0:array(W,0,<2*l,*8,fieldsh(int64<>)), arg1:eq(llvmword(2*l)) -o \
+            \ arg0:array(W,0,<2*l,*8,fieldsh(int64<>)), arg1:true, ret:int64<>";
+
 heapster_export_coq env "arrays_gen.v";
diff --git a/heapster-saw/examples/arrays_proofs.v b/heapster-saw/examples/arrays_proofs.v
index 32e80eaed0..479f8d7a5a 100644
--- a/heapster-saw/examples/arrays_proofs.v
+++ b/heapster-saw/examples/arrays_proofs.v
@@ -212,3 +212,54 @@ Proof.
     repeat f_equal.
     admit. *)
 Admitted.
+
+(* We *really* need a better bitvector library, the lemmas we need are getting pretty ad-hoc *)
+
+Axiom bvSub_1_lt : forall w a, isBvslt w (intToBv w 0) a ->
+                               isBvslt w (bvSub w a (intToBv w 1)) a.
+
+Axiom isBvslt_suc_r : forall w a, isBvslt w a (bvsmax w) ->
+                                  isBvslt w a (bvAdd w a (intToBv w 1)).
+
+Axiom isBvsle_bvSub_inj_pos : forall w a b c, isBvsle w (intToBv w 0) a ->
+                                              isBvsle w (intToBv w 0) b ->
+                                              isBvsle w (intToBv w 0) c ->
+                                              isBvsle w (bvSub w a c) (bvSub w b c) <->
+                                              isBvsle w a b.
+
+Definition even_odd_sums_diff_invar half_len len i :=
+  len = bvMul 64 (intToBv 64 2) half_len /\
+  isBvslt 64 (intToBv 64 0) i.
+
+Lemma no_errors_even_odd_sums_diff :
+  refinesFun even_odd_sums_diff (fun half_len arr => noErrorsSpec).
+Proof.
+  unfold even_odd_sums_diff, even_odd_sums_diff__tuple_fun.
+  Set Printing Depth 1000.
+  prove_refinement_match_letRecM_l.
+  - exact (fun half_len len sum i arr _ _ _ _ =>
+             assumingM (even_odd_sums_diff_invar half_len len i)
+                       noErrorsSpec).
+  unfold even_odd_sums_diff_invar, noErrorsSpec.
+  time "even_odd_sums_diff" prove_refinement.
+  all: try assumption.
+  - enough (isBvult 64 (bvSub 64 a4 (intToBv 64 1)) (bvMul 64 (intToBv 64 2) a1))
+      by (rewrite H in e_maybe; discriminate e_maybe).
+    rewrite <- e_if.
+    assert (isBvsle 64 (intToBv 64 0) a4) by (apply isBvslt_to_isBvsle; eauto).
+    apply isBvult_to_isBvslt_pos; eauto.
+    + change (intToBv 64 0) with (bvSub 64 (intToBv 64 1) (intToBv 64 1)).
+      (* apply isBvsle_bvSub_inj_pos. *)
+      (* I give up I'm done messing around manually with bitvectors for now *)
+      admit.
+    + apply bvSub_1_lt.
+      rewrite e_assuming; reflexivity.
+  - (* (e_if4 is a contradiction) *)
+    admit.
+  - rewrite e_assuming.
+    change (intToBv 64 2) with (bvAdd 64 (intToBv 64 1) (intToBv 64 1)).
+    rewrite <- bvAdd_assoc.
+    rewrite <- isBvslt_suc_r; [ rewrite <- isBvslt_suc_r; [ reflexivity |] |].
+    + admit.
+    + admit.
+Admitted.
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
index 3e18d2eb9b..85afdbc5dc 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Permissions.hs
@@ -951,29 +951,6 @@ zeroOfType _ = error "zeroOfType"
 varFactor :: (1 <= w, KnownNat w) => ExprVar (BVType w) -> BVFactor w
 varFactor = BVFactor $ BV.one knownNat
 
--- | Normalize a bitvector expression @1*x + 0@ to just @x@
-bvNormVar :: PermExpr (BVType w) -> PermExpr (BVType w)
-bvNormVar (PExpr_BV [BVFactor i x] off)
-  | i == BV.one knownNat && off == BV.zero knownNat = PExpr_Var x
-bvNormVar e = e
-
--- | Normalize a bitvector expression, so that every variable has at most one
--- factor and the factors are sorted by variable name. NOTE: we shouldn't
--- actually have to call this if we always construct our expressions with the
--- combinators below.
-bvNormalize :: PermExpr (BVType w) -> PermExpr (BVType w)
-bvNormalize e@(PExpr_Var _) = e
-bvNormalize (PExpr_BV factors off) =
-  PExpr_BV
-  (norm (sortBy (\(BVFactor _ x) (BVFactor _ y) -> compare x y) factors))
-  off
-  where
-    norm [] = []
-    norm ((BVFactor (BV.BV 0) _) : factors') = norm factors'
-    norm ((BVFactor i1 x1) : (BVFactor i2 x2) : factors')
-      | x1 == x2 = norm ((BVFactor (BV.add knownNat i1 i2) x1) : factors')
-    norm (f : factors') = f : norm factors'
-
 -- | Merge two normalized / sorted lists of 'BVFactor's
 bvMergeFactors :: [BVFactor w] -> [BVFactor w] -> [BVFactor w]
 bvMergeFactors fs1 fs2 =
@@ -1298,18 +1275,25 @@ bvIntOfSize _ = bvInt
 bvBV :: (1 <= w, KnownNat w) => BV w -> PermExpr (BVType w)
 bvBV i = PExpr_BV [] i
 
+-- | Build a bitvector expression consisting of a single single 'BVFactor',
+-- i.e. a variable multiplied by some constant
+bvFactorExpr :: (1 <= w, KnownNat w) =>
+                BV w -> ExprVar (BVType w) -> PermExpr (BVType w)
+bvFactorExpr (BV.BV 1) x = PExpr_Var x
+bvFactorExpr i         x = PExpr_BV [BVFactor i x] (BV.zero knownNat)
+
 -- | Add two bitvector expressions
 bvAdd :: (1 <= w, KnownNat w) => PermExpr (BVType w) -> PermExpr (BVType w) ->
          PermExpr (BVType w)
 bvAdd (bvMatch -> (factors1, const1)) (bvMatch -> (factors2, const2)) =
-  bvNormVar $
+  normalizeBVExpr $
   PExpr_BV (bvMergeFactors factors1 factors2) (BV.add knownNat const1 const2)
 
 -- | Multiply a bitvector expression by a bitvector
 bvMultBV :: (1 <= w, KnownNat w) => BV.BV w -> PermExpr (BVType w) ->
             PermExpr (BVType w)
 bvMultBV i_bv (bvMatch -> (factors, off)) =
-  bvNormVar $
+  normalizeBVExpr $
   PExpr_BV (map (\(BVFactor j x) ->
                   BVFactor (BV.mul knownNat i_bv j) x) factors)
   (BV.mul knownNat i_bv off)
@@ -1337,7 +1321,7 @@ bvDiv :: (1 <= w, KnownNat w) => PermExpr (BVType w) -> Integer ->
          PermExpr (BVType w)
 bvDiv (bvMatch -> (factors, off)) n =
   let n_bv = BV.mkBV knownNat n in
-  bvNormVar $
+  normalizeBVExpr $
   PExpr_BV (mapMaybe (\(BVFactor i x) ->
                        if BV.urem i n_bv == BV.zero knownNat then
                          Just (BVFactor (BV.uquot i n_bv) x)
@@ -1350,7 +1334,7 @@ bvMod :: (1 <= w, KnownNat w) => PermExpr (BVType w) -> Integer ->
          PermExpr (BVType w)
 bvMod (bvMatch -> (factors, off)) n =
   let n_bv = BV.mkBV knownNat n in
-  bvNormVar $
+  normalizeBVExpr $
   PExpr_BV (mapMaybe (\f@(BVFactor i _) ->
                        if BV.urem i n_bv /= BV.zero knownNat
                        then Just f else Nothing) factors)
@@ -1364,6 +1348,24 @@ bvMatchFactorPlusConst :: (1 <= w, KnownNat w) =>
 bvMatchFactorPlusConst a e =
   bvMatchConst (bvMod e a) >>= \y -> Just (bvDiv e a, y)
 
+-- | Returns the greatest common divisor of all the coefficients (i.e. offsets
+-- and factor coefficients) of the given bitvectors, returning a negative
+-- number iff all coefficients are <= 0
+bvGCD :: (1 <= w, KnownNat w) =>
+         PermExpr (BVType w) -> PermExpr (BVType w) -> BV w
+bvGCD (bvMatch -> (fs1, off1)) (bvMatch -> (fs2, off2)) =
+  fromMaybe (error "bvGCD: overflow") . BV.mkBVSigned knownNat $
+  foldl' (\d (BVFactor i _) -> d `gcdS` BV.asSigned knownNat i)
+         (foldl' (\d (BVFactor i _) -> d `gcdS` BV.asSigned knownNat i)
+                 (BV.asSigned knownNat off1 `gcdS` BV.asSigned knownNat off2)
+                 fs1)
+         fs2
+  where -- A version of 'gcd' whose return value is negative iff both of
+        -- its arguments are <= 0
+        gcdS :: Integer -> Integer -> Integer
+        gcdS x y | x <= 0 && y <= 0 = - gcd x y
+                 | otherwise        =   gcd x y
+
 -- | Convert an LLVM pointer expression to a variable + optional offset, if this
 -- is possible
 asLLVMOffset :: (1 <= w, KnownNat w) => PermExpr (LLVMPointerType w) ->
@@ -5769,8 +5771,7 @@ mbFactorNameBoundP psubst (mbMatch -> [nuMP| BVFactor (BV.BV mb_n) mb_z |]) =
     Left memb -> case psubstLookup psubst memb of 
                    Nothing -> Left (n, memb)
                    Just e' -> Right (bvMultBV (BV.mkBV knownNat n) e')
-    Right z -> Right (PExpr_BV [BVFactor (BV.mkBV knownNat n) z]
-                               (BV.zero knownNat))
+    Right z -> Right (bvFactorExpr (BV.mkBV knownNat n) z)
 
 
 ----------------------------------------------------------------------
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
index 35b23a423c..81be0726f2 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/SAWTranslation.hs
@@ -2529,12 +2529,12 @@ translateSimplImpl (ps0 :: Proxy ps0) mb_simpl m = case mbMatch mb_simpl of
            [nuP| DistPermsCons _ _ (ValPerm_LLVMArray mb_ap) |] -> return mb_ap
            _ -> error ("translateSimplImpl: SImpl_LLVMArrayFromBlock: "
                        ++ "unexpected form of output permission")
-       (w_term, len_term, elem_tp, ap_tp_trans) <- translateLLVMArrayPerm mb_ap
+       (w_term, _, elem_tp, ap_tp_trans) <- translateLLVMArrayPerm mb_ap
        withPermStackM id
          (\(pctx :>: ptrans_cell) ->
            let arr_term =
                  applyOpenTermMulti (globalOpenTerm "Prelude.singletonBVVec")
-                 [w_term, len_term, elem_tp, transTerm1 ptrans_cell] in
+                 [w_term, elem_tp, transTerm1 ptrans_cell] in
            pctx :>:
            PTrans_Conj [APTrans_LLVMArray $ typeTransF ap_tp_trans [arr_term]])
          m
diff --git a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
index c7405b15da..d0f603566b 100644
--- a/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
+++ b/heapster-saw/src/Verifier/SAW/Heapster/Widening.hs
@@ -282,21 +282,16 @@ widenExpr' tp e1@(asVarOffset -> Just (x1, off1)) e2@(asVarOffset ->
        _ | x1 == x2 && offsetsEq off1 off2 ->
            visitM x1 >> return e1
 
-       -- If we have the same variable but different offsets, e.g., if we are
-       -- widening x &+ bv1 and x &+ bv2, then bind a fresh variable bv for the
-       -- offset and return x &+ bv. Note that we cannot have the same variable
+       -- If we have the same variable but different offsets, we widen them
+       -- using 'widenOffsets'. Note that we cannot have the same variable
        -- x on both sides unless they have been visited, so we can safely
        -- ignore the isv1 and isv2 flags. The complexity of having these two
        -- cases is to find the BVType of one of off1 or off2; because the
        -- previous case did not match, we know at least one is LLVMPermOffset.
        _ | x1 == x2, LLVMPermOffset (exprType -> off_tp) <- off1 ->
-           do off_var <- bindFreshVar off_tp
-              visitM off_var
-              return $ PExpr_LLVMOffset x1 (PExpr_Var off_var)
+           PExpr_LLVMOffset x1 <$> widenOffsets off_tp off1 off2
        _ | x1 == x2, LLVMPermOffset (exprType -> off_tp) <- off2 ->
-           do off_var <- bindFreshVar off_tp
-              visitM off_var
-              return $ PExpr_LLVMOffset x1 (PExpr_Var off_var)
+           PExpr_LLVMOffset x1 <$> widenOffsets off_tp off1 off2
 
        -- If a variable has an eq(e) permission, replace it with e and recurse
        (ValPerm_Eq e1', _, _, _) ->
@@ -453,6 +448,40 @@ widenExprs (CruCtxCons tps tp) (es1 :>: e1) (es2 :>: e2) =
   (:>:) <$> widenExprs tps es1 es2 <*> widenExpr tp e1 e2
 
 
+-- | Widen two bitvector offsets by trying to widen them additively
+-- ('widenBVsAddy'), or if that is not possible, by widening them 
+-- multiplicatively ('widenBVsMulty')
+widenOffsets :: (1 <= w, KnownNat w) => TypeRepr (BVType w) ->
+                PermOffset (LLVMPointerType w) ->
+                PermOffset (LLVMPointerType w) ->
+                WideningM (PermExpr (BVType w))
+widenOffsets tp (llvmPermOffsetExpr -> off1) (llvmPermOffsetExpr -> off2) =
+  widenBVsAddy tp off1 off2 >>= maybe (widenBVsMulty tp off1 off2) return
+
+-- | Widen two bitvectors @bv1@ and @bv2@ additively, i.e. bind a fresh
+-- variable @bv@ and return @(bv2 - bv1) * bv + bv1@, assuming @bv2 - bv1@
+-- is a constant
+widenBVsAddy :: (1 <= w, KnownNat w) => TypeRepr (BVType w) ->
+                PermExpr (BVType w) -> PermExpr (BVType w) ->
+                WideningM (Maybe (PermExpr (BVType w)))
+widenBVsAddy tp bv1 bv2 =
+  case bvMatchConst (bvSub bv2 bv1) of
+    Just d -> do x <- bindFreshVar tp
+                 visitM x
+                 return $ Just (bvAdd (bvFactorExpr d x) bv1)
+    _ -> return Nothing
+
+-- | Widen two bitvectors @bv1@ and @bv2@ multiplicatively, i.e. bind a fresh
+-- variable @bv@ and return @(bvGCD bv1 bv2) * bv@
+widenBVsMulty :: (1 <= w, KnownNat w) => TypeRepr (BVType w) ->
+                 PermExpr (BVType w) -> PermExpr (BVType w) ->
+                 WideningM (PermExpr (BVType w))
+widenBVsMulty tp bv1 bv2 =
+  do x <- bindFreshVar tp
+     visitM x
+     return $ bvFactorExpr (bvGCD bv1 bv2) x
+
+
 -- | Take two block permissions @bp1@ and @bp2@ with the same offset and use
 -- 'splitLLVMBlockPerm' to remove any parts of them that do not overlap,
 -- returning some @bp1'@ and @bp2'@ with the same range, along with additional
diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
index dfa7149c6e..24fdb1a580 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/SAWCoreBitvectors.v
@@ -226,9 +226,11 @@ Hint Rewrite bvNeg_msb : SAWCoreBitvectors_eqs.
 Lemma bvNeg_bvAdd_distrib w a b : bvNeg w (bvAdd w a b) = bvAdd w (bvNeg w a) (bvNeg w b).
 Admitted.
 
+(* FIXME This is false if a <= 0 *)
 Lemma bvslt_bvSub_r w a b : isBvslt w a b <-> isBvslt w (intToBv w 0) (bvSub w b a).
 Admitted.
 
+(* FIXME This is false if a <= 0 *)
 Lemma bvslt_bvSub_l w a b : isBvslt w a b <-> isBvslt w (bvSub w a b) (intToBv w 0).
 Admitted.