diff --git a/base/src/Data/Macaw/CFG/Core.hs b/base/src/Data/Macaw/CFG/Core.hs
index 47e3f611..1cf97a71 100644
--- a/base/src/Data/Macaw/CFG/Core.hs
+++ b/base/src/Data/Macaw/CFG/Core.hs
@@ -331,6 +331,8 @@ data Value arch ids tp
    . (tp ~ BVType n, 1 <= n)
    => BVValue !(NatRepr n) !Integer
      -- ^ A constant bitvector
+     --
+     -- The integer should be between 0 and 2^n-1.
    | (tp ~ BoolType)
    => BoolValue !Bool
      -- ^ A constant Boolean
diff --git a/symbolic/src/Data/Macaw/Symbolic.hs b/symbolic/src/Data/Macaw/Symbolic.hs
index 1538e769..be11b6b2 100644
--- a/symbolic/src/Data/Macaw/Symbolic.hs
+++ b/symbolic/src/Data/Macaw/Symbolic.hs
@@ -178,8 +178,6 @@ mkBlocksCFG archFns halloc memBaseVarMap nm posFn macawBlocks = do
   mkCrucCFG archFns halloc nm $ do
     addBlocksCFG archFns memBaseVarMap posFn macawBlocks
 
-type FunBlockMap arch s = Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
-
 mkFunCFG :: forall s arch ids
          .  MacawSymbolicArchFunctions arch
             -- ^ Architecture specific functions.
@@ -197,17 +195,17 @@ mkFunCFG :: forall s arch ids
 mkFunCFG archFns halloc memBaseVarMap nm posFn fn = do
   mkCrucCFG archFns halloc nm $ do
     let insSentences :: M.ArchSegmentOff arch
-                     -> (FunBlockMap arch s,Int)
+                     -> (BlockLabelMap arch s,Int)
                      -> [M.StatementList arch ids]
-                     -> (FunBlockMap arch s,Int)
+                     -> (BlockLabelMap arch s,Int)
         insSentences _ m [] = m
         insSentences base (m,c) (s:r) =
           insSentences base
                        (Map.insert (base,M.stmtsIdent s) (CR.Label c) m,c+1)
                        (nextStatements (M.stmtsTerm s) ++ r)
-    let insBlock :: (FunBlockMap arch s,Int) -> M.ParsedBlock arch ids -> (FunBlockMap arch s,Int)
+    let insBlock :: (BlockLabelMap arch s,Int) -> M.ParsedBlock arch ids -> (BlockLabelMap arch s,Int)
         insBlock m b = insSentences (M.pblockAddr b) m [M.blockStatementList b]
-    let blockLabelMap :: FunBlockMap arch s
+    let blockLabelMap :: BlockLabelMap arch s
         blockLabelMap = fst $ foldl' insBlock (Map.empty,0) (Map.elems (fn^.M.parsedBlocks))
     let regReg = CR.Reg { CR.regPosition = posFn (M.discoveredFunAddr fn)
                         , CR.regId = 0
diff --git a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
index 4acda4ed..409054cd 100644
--- a/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
+++ b/symbolic/src/Data/Macaw/Symbolic/CrucGen.hs
@@ -38,6 +38,7 @@ module Data.Macaw.Symbolic.CrucGen
   , MacawMonad
   , runMacawMonad
   , addMacawBlock
+  , BlockLabelMap
   , addParsedBlock
   , nextStatements
   , valueToCrucible
@@ -738,8 +739,11 @@ setMachineRegs newRegs = do
   regReg <- gets crucRegisterReg
   addStmt $ CR.SetReg regReg newRegs
 
-addMacawParsedTermStmt :: Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
-                          -- ^ Map from block addresses to starting label
+-- | Map from block information to Crucible label (used to generate term statements)
+type BlockLabelMap arch s = Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
+
+addMacawParsedTermStmt :: BlockLabelMap arch s
+                          -- ^ Block label map for this function
                        -> M.ArchSegmentOff arch
                           -- ^ Address of this block
                        -> M.ParsedTermStmt arch ids
@@ -760,8 +764,13 @@ addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do
     M.ParsedJump regs nextAddr -> do
       setMachineRegs =<< createRegStruct regs
       addTermStmt $ CR.Jump (parsedBlockLabel blockLabelMap nextAddr 0)
-    M.ParsedLookupTable _regs _idx _possibleAddrs -> do
-      error "Crucible symbolic generator does not yet support lookup tables."
+    M.ParsedLookupTable regs _idx _possibleAddrs -> do
+      setMachineRegs =<< createRegStruct regs
+      let cond = undefined
+      -- TODO: Add ability in CrucGen to generate new labels and add new blocks.
+      let tlbl = undefined
+      let flbl = undefined
+      addTermStmt $! CR.Br cond tlbl flbl
     M.ParsedReturn regs -> do
       regValues <- createRegStruct regs
       addTermStmt $ CR.Return regValues
@@ -771,7 +780,6 @@ addMacawParsedTermStmt blockLabelMap thisAddr tstmt = do
       let flbl = parsedBlockLabel blockLabelMap thisAddr (M.stmtsIdent f)
       addTermStmt $! CR.Br crucCond tlbl flbl
     M.ParsedArchTermStmt aterm regs _mret -> do
-      archFns <- gets translateFns
       crucGenArchTermStmt archFns aterm regs
     M.ParsedTranslateError msg -> do
       msgVal <- crucibleValue (C.TextLit msg)
@@ -789,7 +797,7 @@ nextStatements tstmt =
 addStatementList :: MacawSymbolicArchFunctions arch
                  -> MemSegmentMap (M.ArchAddrWidth arch)
                  -- ^ Base address map
-                 -> Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
+                 -> BlockLabelMap arch s
                  -- ^ Map from block index to Crucible label
                  -> M.ArchSegmentOff arch
                  -- ^ Address of block that starts statements
@@ -822,7 +830,7 @@ addParsedBlock :: forall arch ids s
                .  MacawSymbolicArchFunctions arch
                -> MemSegmentMap (M.ArchAddrWidth arch)
                -- ^ Base address map
-               -> Map (M.ArchSegmentOff arch, Word64) (CR.Label s)
+               -> BlockLabelMap arch s
                -- ^ Map from block index to Crucible label
                -> (M.ArchSegmentOff arch -> C.Position)
                -- ^ Function for generating position from offset from start of this block.
@@ -836,4 +844,5 @@ addParsedBlock tfns baseAddrMap blockLabelMap posFn regReg b = do
   let thisPosFn :: M.ArchAddrWord arch -> C.Position
       thisPosFn off = posFn r
         where Just r = M.incSegmentOff base (toInteger off)
-  addStatementList tfns baseAddrMap blockLabelMap (M.pblockAddr b) thisPosFn regReg [(0, M.blockStatementList b)] []
+  addStatementList tfns baseAddrMap blockLabelMap
+    (M.pblockAddr b) thisPosFn regReg [(0, M.blockStatementList b)] []
diff --git a/x86/src/Data/Macaw/X86/Generator.hs b/x86/src/Data/Macaw/X86/Generator.hs
index 1fa32929..c36215ba 100644
--- a/x86/src/Data/Macaw/X86/Generator.hs
+++ b/x86/src/Data/Macaw/X86/Generator.hs
@@ -52,7 +52,8 @@ module Data.Macaw.X86.Generator
   , asApp
   , asArchFn
   , asBoolLit
-  , asBVLit
+  , asUnsignedBVLit
+  , asSignedBVLit
   , eval
   , getRegValue
   , setReg
@@ -79,6 +80,7 @@ import           Data.Maybe
 import           Data.Parameterized.Classes
 import           Data.Parameterized.Map (MapF)
 import qualified Data.Parameterized.Map as MapF
+import           Data.Parameterized.NatRepr
 import           Data.Parameterized.Nonce
 import           Data.Parameterized.TraversableFC
 import           Data.Sequence (Seq)
@@ -137,9 +139,15 @@ asBoolLit :: Expr ids BoolType -> Maybe Bool
 asBoolLit (ValueExpr (BoolValue b)) = Just b
 asBoolLit _ = Nothing
 
-asBVLit :: Expr ids (BVType w) -> Maybe Integer
-asBVLit (ValueExpr (BVValue _ v)) = Just v
-asBVLit _ = Nothing
+-- | If expression is a literal bitvector, then return as an unsigned integer.
+asUnsignedBVLit :: Expr ids (BVType w) -> Maybe Integer
+asUnsignedBVLit (ValueExpr (BVValue w v)) = Just (toUnsigned w v)
+asUnsignedBVLit _ = Nothing
+
+-- | If expression is a literal bitvector, then return as an signed integer.
+asSignedBVLit :: Expr ids (BVType w) -> Maybe Integer
+asSignedBVLit (ValueExpr (BVValue w v)) = Just (toSigned w v)
+asSignedBVLit _ = Nothing
 
 ------------------------------------------------------------------------
 -- PreBlock
diff --git a/x86/src/Data/Macaw/X86/Monad.hs b/x86/src/Data/Macaw/X86/Monad.hs
index e149d0b1..b70d16de 100644
--- a/x86/src/Data/Macaw/X86/Monad.hs
+++ b/x86/src/Data/Macaw/X86/Monad.hs
@@ -912,8 +912,8 @@ bvLit n v = ValueExpr $ mkLit n (toInteger v)
 (.+) :: 1 <= n => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
 x .+ y
   -- Eliminate add 0
-  | Just 0 <- asBVLit y = x
-  | Just 0 <- asBVLit x = y
+  | Just 0 <- asUnsignedBVLit y = x
+  | Just 0 <- asUnsignedBVLit x = y
 
   -- Constant folding.
   | ValueExpr (BVValue w xv) <- x
@@ -933,11 +933,11 @@ x .+ y
   | ValueExpr (BVValue _ _) <- x = y .+ x
 
   -- Reorganize addition by constant to offset.
-  | Just (BVAdd w x_base (asBVLit -> Just x_off)) <- asApp x
+  | Just (BVAdd w x_base (asUnsignedBVLit -> Just x_off)) <- asApp x
   , ValueExpr (BVValue _ y_off) <- y
   = x_base .+ bvLit w (x_off + y_off)
 
-  | Just (BVAdd w y_base (asBVLit -> Just y_off)) <- asApp y
+  | Just (BVAdd w y_base (asUnsignedBVLit -> Just y_off)) <- asApp y
   , ValueExpr (BVValue _ x_off) <- x
   = y_base .+ bvLit w (x_off + y_off)
 
@@ -953,12 +953,12 @@ x .- y
 -- | Performs a multiplication of two bitvector values.
 (.*) :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
 x .* y
-  | Just 0 <- asBVLit x = x
-  | Just 1 <- asBVLit x = y
-  | Just 0 <- asBVLit y = y
-  | Just 1 <- asBVLit y = x
+  | Just 0 <- asUnsignedBVLit x = x
+  | Just 1 <- asUnsignedBVLit x = y
+  | Just 0 <- asUnsignedBVLit y = y
+  | Just 1 <- asUnsignedBVLit y = x
 
-  | Just xv <- asBVLit x, Just yv <- asBVLit y =
+  | Just xv <- asUnsignedBVLit x, Just yv <- asUnsignedBVLit y =
       bvLit (typeWidth x) (xv * yv)
   | otherwise = app $ BVMul (typeWidth x) x y
 
@@ -969,7 +969,7 @@ bvNeg n = bvLit (typeWidth n) 0 .- n
 -- | Bitwise complement
 bvComplement :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n)
 bvComplement x
-  | Just xv <- asBVLit x = bvLit (typeWidth x) (Bits.complement xv)
+  | Just xv <- asUnsignedBVLit x = bvLit (typeWidth x) (Bits.complement xv)
     -- not (not p) = p
   | Just (BVComplement _ y) <- asApp x = y
   | otherwise = app $ BVComplement (typeWidth x) x
@@ -977,35 +977,35 @@ bvComplement x
 -- | Bitwise and
 (.&.) :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
 x .&. y
-  | Just xv <- asBVLit x, Just yv <- asBVLit y =
+  | Just xv <- asUnsignedBVLit x, Just yv <- asUnsignedBVLit y =
       bvLit (typeWidth x) (xv Bits..&. yv)
   -- Eliminate and when one argument is maxUnsigned
-  | Just xv <- asBVLit x, xv == maxUnsigned (typeWidth x) = y
-  | Just yv <- asBVLit y, yv == maxUnsigned (typeWidth x) = x
+  | Just xv <- asUnsignedBVLit x, xv == maxUnsigned (typeWidth x) = y
+  | Just yv <- asUnsignedBVLit y, yv == maxUnsigned (typeWidth x) = x
   -- Cancel when and with 0.
-  | Just 0 <- asBVLit x = x
-  | Just 0 <- asBVLit y = y
+  | Just 0 <- asUnsignedBVLit x = x
+  | Just 0 <- asUnsignedBVLit y = y
   -- Idempotence
   | x == y = x
 
   -- Make literal the second argument (simplifies later cases)
-  | isJust (asBVLit x) = assert (isNothing (asBVLit y)) $ y .&. x
+  | isJust (asUnsignedBVLit x) = assert (isNothing (asUnsignedBVLit y)) $ y .&. x
 
   --(x1 .&. x2) .&. y = x1 .&. (x2 .&. y) -- Only apply when x2 and y is a lit
-  | isJust (asBVLit y)
+  | isJust (asUnsignedBVLit y)
   , Just (BVAnd _ x1 x2) <- asApp x
-  , isJust (asBVLit x2) =
+  , isJust (asUnsignedBVLit x2) =
     x1 .&. (x2 .&. y)
 
   -- (x1 .|. x2) .&. y = (x1 .&. y) .|. (x2 .&. y) -- Only apply when y and x2 is a lit.
-  | isJust (asBVLit y)
+  | isJust (asUnsignedBVLit y)
   , Just (BVOr _ x1 x2) <- asApp x
-  ,  isJust (asBVLit x2) =
+  ,  isJust (asUnsignedBVLit x2) =
       (x1 .&. y) .|. (x2 .&. y)
   -- x .&. (y1 .|. y2) = (y1 .&. x) .|. (y2 .&. x) -- Only apply when x and y2 is a lit.
-  | isJust (asBVLit x)
+  | isJust (asUnsignedBVLit x)
   , Just (BVOr _ y1 y2) <- asApp y
-  , isJust (asBVLit y2) =
+  , isJust (asUnsignedBVLit y2) =
       (y1 .&. x) .|. (y2 .&. x)
 
   -- Default case
@@ -1014,14 +1014,14 @@ x .&. y
 -- | Bitwise or
 (.|.) :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
 x .|. y
-  | Just xv <- asBVLit x, Just yv <- asBVLit y =
+  | Just xv <- asUnsignedBVLit x, Just yv <- asUnsignedBVLit y =
       bvLit (typeWidth x) (xv Bits..|. yv)
   -- Cancel or when one argument is maxUnsigned
-  | Just xv <- asBVLit x, xv == maxUnsigned (typeWidth x) = x
-  | Just yv <- asBVLit y, yv == maxUnsigned (typeWidth x) = y
+  | Just xv <- asUnsignedBVLit x, xv == maxUnsigned (typeWidth x) = x
+  | Just yv <- asUnsignedBVLit y, yv == maxUnsigned (typeWidth x) = y
   -- Eliminate "or" when one argument is 0
-  | Just 0 <- asBVLit x = y
-  | Just 0 <- asBVLit y = x
+  | Just 0 <- asUnsignedBVLit x = y
+  | Just 0 <- asUnsignedBVLit y = x
   -- Idempotence
   | x == y = x
   -- Default case
@@ -1031,8 +1031,8 @@ x .|. y
 bvXor :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
 bvXor x y
   -- Eliminate xor with 0.
-  | Just 0 <- asBVLit x = y
-  | Just 0 <- asBVLit y = x
+  | Just 0 <- asUnsignedBVLit x = y
+  | Just 0 <- asUnsignedBVLit y = x
   -- Eliminate xor with self.
   | x == y = bvLit (typeWidth x) (0::Integer)
   -- If this is a single bit comparison with a constant, resolve to Boolean operation.
@@ -1054,7 +1054,7 @@ x .=. y
   | ValueExpr BVValue{} <- x  = y .=. x
 
   -- Rewrite "base + offset = constant" to "base = constant - offset".
-  | Just (BVAdd w x_base (asBVLit -> Just x_off)) <- asApp x
+  | Just (BVAdd w x_base (asUnsignedBVLit -> Just x_off)) <- asApp x
   , ValueExpr (BVValue _ yv) <- y =
       app $ Eq x_base (bvLit w (yv - x_off))
       -- Rewrite "u - v == c" to "u = c + v".
@@ -1184,8 +1184,8 @@ bvRor v n = bvShr v n .|. bvShl v bits_less_n
 -- and right shift moves bits to lower-order positions.
 bvShr :: 1 <= n => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
 bvShr x y
-  | Just 0 <- asBVLit y = x
-  | Just 0 <- asBVLit x = x
+  | Just 0 <- asUnsignedBVLit y = x
+  | Just 0 <- asUnsignedBVLit x = x
   | otherwise = app $ BVShr (typeWidth x) x y
 
 bvSar :: 1 <= n => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
@@ -1193,20 +1193,20 @@ bvSar x y = app $ BVSar (typeWidth x) x y
 
 bvShl :: 1 <= n => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids (BVType n)
 bvShl x y
-    | Just 0 <- asBVLit y = x
+    | Just 0 <- asUnsignedBVLit y = x
 
-    | Just xv <- asBVLit x
-    , Just yv <- asBVLit y =
+    | Just xv <- asUnsignedBVLit x
+    , Just yv <- asUnsignedBVLit y =
       assert (yv <= toInteger (maxBound :: Int)) $
         bvLit (typeWidth x) (xv `Bits.shiftL` fromInteger yv)
 
       -- Replace "(x >> c) << c" with (x .&. - 2^c)
-    | Just yv <- asBVLit y
-    , Just (BVShr w x_base (asBVLit -> Just x_shft)) <- asApp x
+    | Just yv <- asUnsignedBVLit y
+    , Just (BVShr w x_base (asUnsignedBVLit -> Just x_shft)) <- asApp x
     , x_shft == yv =
       x_base .&. bvLit w (negate (2^x_shft) ::Integer)
 
-    | Just yv <- asBVLit y
+    | Just yv <- asUnsignedBVLit y
     , yv >= natValue (typeWidth x) = bvLit (typeWidth x) (0 :: Integer)
 
     | otherwise = app $ BVShl (typeWidth x) x y
@@ -1216,7 +1216,7 @@ bvShl x y
 -- 'uext'' docs.
 bvTrunc' :: (1 <= m, m+1 <= n) => NatRepr m -> Expr ids (BVType n) -> Expr ids (BVType m)
 bvTrunc' w e0
-  | Just v <- asBVLit e0 =
+  | Just v <- asUnsignedBVLit e0 =
       bvLit w v
   | Just Refl <- testEquality (typeWidth e0) w =
       e0
@@ -1261,37 +1261,43 @@ bvTrunc w e =
     Right Refl -> e
 
 -- | Unsigned less than
-bvUlt :: Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
+bvUlt :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
 bvUlt x y
-  | Just xv <- asBVLit x, Just yv <- asBVLit y = boolValue (xv < yv)
+  | Just xv <- asUnsignedBVLit x, Just yv <- asUnsignedBVLit y = boolValue (xv < yv)
   | x == y = false
-  | otherwise =
-      case typeRepr x of
-        BVTypeRepr _ -> app $ BVUnsignedLt x y
+  | otherwise =  app $ BVUnsignedLt x y
 
 -- | Unsigned less than or equal.
-bvUle :: Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
-bvUle x y = boolNot (bvUlt y x)
+bvUle :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
+bvUle x y
+  | Just xv <- asUnsignedBVLit x, Just yv <- asUnsignedBVLit y = boolValue (xv <= yv)
+  | x == y = true
+  | otherwise = app $ BVUnsignedLe x y
 
 -- | Signed less than
 bvSlt :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
 bvSlt x y
-  | Just xv <- asBVLit x, Just yv <- asBVLit y = boolValue (xv < yv)
+  | Just xv <- asSignedBVLit x, Just yv <- asSignedBVLit y = boolValue (xv < yv)
   | x == y = false
-  | otherwise =
-      case typeRepr x of
-        BVTypeRepr _ -> app $ BVSignedLt x y
+  | otherwise = app $ BVSignedLt x y
+
+-- | Signed less than
+bvSle :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
+bvSle x y
+  | Just xv <- asSignedBVLit x, Just yv <- asSignedBVLit y = boolValue (xv <= yv)
+  | x == y = true
+  | otherwise = app $ BVSignedLe x y
 
 -- | Returns bit at index given by second argument, 0 being lsb
 -- If the bit index is greater than or equal to n, then the result is zero.
 bvBit :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
 bvBit x y
-  | Just xv <- asBVLit x
-  , Just yv <- asBVLit y =
+  | Just xv <- asUnsignedBVLit x
+  , Just yv <- asUnsignedBVLit y =
       boolValue (xv `Bits.testBit` fromInteger yv)
   | Just (Trunc xe w) <- asApp x
   , Just LeqProof <- testLeq n1 (typeWidth xe)
-  , Just yv <- asBVLit y = assert (0 <= yv && yv < natValue w) $
+  , Just yv <- asUnsignedBVLit y = assert (0 <= yv && yv < natValue w) $
     bvBit xe (ValueExpr (BVValue (typeWidth xe) yv))
 
   | otherwise =
@@ -1332,7 +1338,7 @@ sext w e =
 uext' :: (1 <= m, m+1 <= n, 1 <= n) => NatRepr n -> Expr ids (BVType m) -> Expr ids (BVType n)
 uext' w e0
   -- Literal case
-  | Just v <- asBVLit e0 =
+  | Just v <- asUnsignedBVLit e0 =
     let w0 = typeWidth e0
      in withLeqProof (leqTrans (leqProof n1 w0) (ltProof w0 w)) $
         bvLit w v
@@ -1371,7 +1377,7 @@ least_byte = bvTrunc knownNat
 -- of the result is different.
 sadc_overflows :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType -> Expr ids BoolType
 sadc_overflows x y c
-  | Just 0 <- asBVLit y, Just False <- asBoolLit c = false
+  | Just 0 <- asUnsignedBVLit y, Just False <- asBoolLit c = false
   | otherwise = app $ SadcOverflows x y c
 
 -- | Return true expression is signed add overflows.  See
@@ -1382,7 +1388,7 @@ sadd_overflows x y = sadc_overflows x y false
 -- | Return true expression if a unsigned add-with carry would overflow.
 uadc_overflows :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType -> Expr ids BoolType
 uadc_overflows x y c
-  | Just 0 <- asBVLit y, Just False <- asBoolLit c = false
+  | Just 0 <- asUnsignedBVLit y, Just False <- asBoolLit c = false
   | otherwise = app $ UadcOverflows x y c
 
 -- | Return true expression is unsigned add overflows.  See
@@ -1400,7 +1406,7 @@ usbb_overflows :: (1 <= n)
                  -> Expr ids BoolType
                  -> Expr ids BoolType
 usbb_overflows x y c
-  | Just 0 <- asBVLit y, Just False <- asBoolLit c = false
+  | Just 0 <- asUnsignedBVLit y, Just False <- asBoolLit c = false
     -- If the borrow bit is zero, this is equivalent to unsigned x < y.
   | Just False <- asBoolLit c = bvUlt x y
   | otherwise = app $ UsbbOverflows x y c
@@ -1422,9 +1428,9 @@ ssbb_overflows :: (1 <= n)
                  -> Expr ids BoolType
                  -> Expr ids BoolType
 ssbb_overflows x y c
-  | Just 0 <- asBVLit y, Just False <- asBoolLit c = false
+  | Just 0 <- asUnsignedBVLit y, Just False <- asBoolLit c = false
     -- If the borrow bit is zero, this is equivalent to signed x < y.
-    -- FIXME: not true? | Just 0 <- asBVLit c = app $ BVSignedLt x y
+    -- FIXME: not true? | Just 0 <- asUnsignedBVLit c = app $ BVSignedLt x y
   | otherwise = app $ SsbbOverflows x y c
 
 -- | Return true expression is signed sub overflows.
@@ -1527,9 +1533,6 @@ boolXor x y
   -- Default case.
   | otherwise = app $ XorApp x y
 
-bvSle :: (1 <= n) => Expr ids (BVType n) -> Expr ids (BVType n) -> Expr ids BoolType
-bvSle x y = app (BVSignedLe x y)
-
 -- | Construct a literal bit vector.  The result is undefined if the
 -- literal does not fit withint the given number of bits.
 bvKLit :: (KnownNat n, 1 <= n) => Integer -> Expr ids (BVType n)
diff --git a/x86/src/Data/Macaw/X86/Semantics.hs b/x86/src/Data/Macaw/X86/Semantics.hs
index 2e37cd5f..d85dd698 100644
--- a/x86/src/Data/Macaw/X86/Semantics.hs
+++ b/x86/src/Data/Macaw/X86/Semantics.hs
@@ -765,8 +765,7 @@ def_sh mnem val_setter cf_setter of_setter = defBinary mnem $ \_ii loc val -> do
 def_shl :: InstructionDef
 def_shl = def_sh "shl" bvShl set_cf set_of
   where set_cf w v i =
-           (i `bvUle` bvLit n8 (natValue w))
-             .&&. bvBit v (bvLit w (natValue w) .- uext w i)
+           (i `bvUle` bvLit n8 (natValue w)) .&&. bvBit v (bvLit w (natValue w) .- uext w i)
         set_of v _ =  msb v
 
 def_shr :: InstructionDef