diff --git a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
index a2c8d4a5b..7f17718bd 100644
--- a/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
+++ b/docs/ProgrammingCryptol/crashCourse/CrashCourse.tex
@@ -791,7 +791,7 @@ \subsection{Appending and indexing}
   []
   invalid sequence index: 12
    -- Backtrace --
-  (Cryptol::@) called at Cryptol:870:14--870:20
+  (Cryptol::@) called at Cryptol:875:14--875:20
   (Cryptol::@@) called at <interactive>:9:1--9:28
   [9, 8, 7, 6, 5, 4, 3, 2, 1, 0]
   9
diff --git a/lib/Cryptol.cry b/lib/Cryptol.cry
index 14b79f73a..8264abf4b 100644
--- a/lib/Cryptol.cry
+++ b/lib/Cryptol.cry
@@ -734,6 +734,11 @@ primitive (>>$) : {n, ix} (fin n, n >= 1, Integral ix) => [n] -> ix -> [n]
  */
 primitive lg2 : {n} (fin n) => [n] -> [n]
 
+/**
+ * Convert a signed 2's complement bitvector to an integer.
+ */
+primitive toSignedInteger : {n} (fin n, n >= 1) => [n] -> Integer
+
 
 // Rational specific operations ----------------------------------------------
 
diff --git a/src/Cryptol/Backend.hs b/src/Cryptol/Backend.hs
index 5526b1192..d132e5b69 100644
--- a/src/Cryptol/Backend.hs
+++ b/src/Cryptol/Backend.hs
@@ -614,6 +614,12 @@ class MonadIO (SEval sym) => Backend sym where
     SWord sym ->
     SEval sym (SInteger sym)
 
+  -- | Construct a signed integer value from the given packed word.
+  wordToSignedInt ::
+    sym ->
+    SWord sym ->
+    SEval sym (SInteger sym)
+
   -- ==== Integer operations ====
 
   -- | Addition of unbounded integers.
diff --git a/src/Cryptol/Backend/Concrete.hs b/src/Cryptol/Backend/Concrete.hs
index 3a800fe4a..348ef63b8 100644
--- a/src/Cryptol/Backend/Concrete.hs
+++ b/src/Cryptol/Backend/Concrete.hs
@@ -185,6 +185,7 @@ instance Backend Concrete where
   integerAsLit _ = Just
 
   wordToInt _ (BV _ x) = pure x
+  wordToSignedInt _ (BV w x) = pure $! signedValue w x
   wordFromInt _ w x = pure $! mkBv w x
 
   packWord _ bits = pure $! BV (toInteger w) a
diff --git a/src/Cryptol/Backend/SBV.hs b/src/Cryptol/Backend/SBV.hs
index e18a195d8..5ad5bd1dc 100644
--- a/src/Cryptol/Backend/SBV.hs
+++ b/src/Cryptol/Backend/SBV.hs
@@ -293,6 +293,7 @@ instance Backend SBV where
   wordLg2 _ a = sLg2 a
 
   wordToInt _ x = pure $! svToInteger x
+  wordToSignedInt _ x = pure $! svToInteger (svSign x)
   wordFromInt _ w i = pure $! svFromInteger w i
 
   intEq _ a b = pure $! svEqual a b
diff --git a/src/Cryptol/Backend/What4.hs b/src/Cryptol/Backend/What4.hs
index 11731522a..fe0f9c1ae 100644
--- a/src/Cryptol/Backend/What4.hs
+++ b/src/Cryptol/Backend/What4.hs
@@ -362,6 +362,7 @@ instance W4.IsSymExprBuilder sym => Backend (What4 sym) where
         liftIO (SW.bvSRem (w4 sym) x y)
 
   wordToInt sym x = liftIO (SW.bvToInteger (w4 sym) x)
+  wordToSignedInt sym x = liftIO (SW.sbvToInteger (w4 sym) x)
   wordFromInt sym width i = liftIO (SW.integerToBV (w4 sym) i width)
 
   intPlus   sym x y  = liftIO $ W4.intAdd (w4 sym) x y
diff --git a/src/Cryptol/Eval/Generic.hs b/src/Cryptol/Eval/Generic.hs
index 005bc8754..6045d4e31 100644
--- a/src/Cryptol/Eval/Generic.hs
+++ b/src/Cryptol/Eval/Generic.hs
@@ -716,6 +716,13 @@ smodV sym  =
   PWordFun \y ->
   PPrim (VWord w . wordVal <$> wordSignedMod sym x y)
 
+{-# SPECIALIZE toSignedIntegerV :: Concrete -> Prim Concrete #-}
+toSignedIntegerV :: Backend sym => sym -> Prim sym
+toSignedIntegerV sym =
+  PFinPoly \_w ->
+  PWordFun \x ->
+  PPrim (VInteger <$> wordToSignedInt sym x)
+
 -- Cmp -------------------------------------------------------------------------
 
 {-# SPECIALIZE cmpValue ::
@@ -2031,6 +2038,9 @@ genericPrimTable sym getEOpts =
                     unary (roundToEvenV sym))
 
     -- Bitvector specific operations
+  , ("toSignedInteger"
+                  , {-# SCC "Prelude::toSignedInteger" #-}
+                    toSignedIntegerV sym)
   , ("/$"         , {-# SCC "Prelude::(/$)" #-}
                     sdivV sym)
   , ("%$"         , {-# SCC "Prelude::(%$)" #-}
diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout
index 6f88b3458..f7afeafff 100644
--- a/tests/issues/T146.icry.stdout
+++ b/tests/issues/T146.icry.stdout
@@ -4,15 +4,15 @@ Loading module Main
 
 [error] at T146.cry:1:18--6:10:
   The type ?a is not sufficiently polymorphic.
-    It cannot depend on quantified variables: fv`828
+    It cannot depend on quantified variables: fv`829
     When checking type of field 'v0'
   where
   ?a is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
-  fv`828 is signature variable 'fv' at T146.cry:11:10--11:12
+  fv`829 is signature variable 'fv' at T146.cry:11:10--11:12
 [error] at T146.cry:5:19--5:24:
   The type ?b is not sufficiently polymorphic.
-    It cannot depend on quantified variables: fv`828
+    It cannot depend on quantified variables: fv`829
     When checking signature variable 'fv'
   where
   ?b is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
-  fv`828 is signature variable 'fv' at T146.cry:11:10--11:12
+  fv`829 is signature variable 'fv' at T146.cry:11:10--11:12
diff --git a/tests/issues/issue1024.icry.stdout b/tests/issues/issue1024.icry.stdout
index 6fa3adb38..e17455a4d 100644
--- a/tests/issues/issue1024.icry.stdout
+++ b/tests/issues/issue1024.icry.stdout
@@ -13,20 +13,20 @@ Loading module Main
     Unused name: g
 
 [error] at issue1024a.cry:1:6--1:11:
-  Illegal kind assigned to type variable: f`825
+  Illegal kind assigned to type variable: f`826
   Unexpected: # -> *
   where
-  f`825 is signature variable 'f' at issue1024a.cry:1:12--1:24
+  f`826 is signature variable 'f' at issue1024a.cry:1:12--1:24
 [error] at issue1024a.cry:2:6--2:13:
-  Illegal kind assigned to type variable: f`826
+  Illegal kind assigned to type variable: f`827
   Unexpected: Prop
   where
-  f`826 is signature variable 'f' at issue1024a.cry:2:14--2:24
+  f`827 is signature variable 'f' at issue1024a.cry:2:14--2:24
 [error] at issue1024a.cry:4:13--4:49:
-  Illegal kind assigned to type variable: f`828
+  Illegal kind assigned to type variable: f`829
   Unexpected: # -> *
   where
-  f`828 is signature variable 'f' at issue1024a.cry:4:22--4:32
+  f`829 is signature variable 'f' at issue1024a.cry:4:22--4:32
 Loading module Cryptol
 Loading module Main
 0xffff
diff --git a/tests/issues/issue103.icry.stdout b/tests/issues/issue103.icry.stdout
index 1e5c34c41..f8e810618 100644
--- a/tests/issues/issue103.icry.stdout
+++ b/tests/issues/issue103.icry.stdout
@@ -2,7 +2,7 @@ Loading module Cryptol
 
 Run-time error: undefined
 -- Backtrace --
-Cryptol::error called at Cryptol:1040:13--1040:18
+Cryptol::error called at Cryptol:1045:13--1045:18
 Cryptol::undefined called at issue103.icry:1:9--1:18
 Using exhaustive testing.
 Testing... ERROR for the following inputs:
diff --git a/tests/issues/issue226.icry.stdout b/tests/issues/issue226.icry.stdout
index 94139b152..6752753b0 100644
--- a/tests/issues/issue226.icry.stdout
+++ b/tests/issues/issue226.icry.stdout
@@ -207,6 +207,7 @@ Symbols
     tail : {n, a} [1 + n]a -> [n]a
     take : {front, back, a} [front + back]a -> [front]a
     toInteger : {a} (Integral a) => a -> Integer
+    toSignedInteger : {n} (fin n, n >= 1) => [n] -> Integer
     trace : {n, a, b} (fin n) => String n -> a -> b -> b
     traceVal : {n, a} (fin n) => String n -> a -> a
     transpose : {rows, cols, a} [rows][cols]a -> [cols][rows]a
diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout
index 1c4211fe1..182171248 100644
--- a/tests/issues/issue290v2.icry.stdout
+++ b/tests/issues/issue290v2.icry.stdout
@@ -4,9 +4,9 @@ Loading module Main
 
 [error] at issue290v2.cry:2:1--2:19:
   Unsolved constraints:
-    • n`825 == 1
+    • n`826 == 1
         arising from
         checking a pattern: type of 1st argument of Main::minMax
         at issue290v2.cry:2:8--2:11
   where
-  n`825 is signature variable 'n' at issue290v2.cry:1:11--1:12
+  n`826 is signature variable 'n' at issue290v2.cry:1:11--1:12
diff --git a/tests/issues/issue723.icry.stdout b/tests/issues/issue723.icry.stdout
index c383045b8..a391ffdb8 100644
--- a/tests/issues/issue723.icry.stdout
+++ b/tests/issues/issue723.icry.stdout
@@ -10,9 +10,9 @@ Loading module Main
       assuming
         • fin k
       the following constraints hold:
-        • k == n`825
+        • k == n`826
             arising from
             matching types
             at issue723.cry:7:17--7:19
   where
-  n`825 is signature variable 'n' at issue723.cry:1:6--1:7
+  n`826 is signature variable 'n' at issue723.cry:1:6--1:7
diff --git a/tests/modsys/T16.icry.stdout b/tests/modsys/T16.icry.stdout
index 545eec073..72b798362 100644
--- a/tests/modsys/T16.icry.stdout
+++ b/tests/modsys/T16.icry.stdout
@@ -5,5 +5,5 @@ Loading module T16::B
 
 [error] at ./T16/B.cry:5:5--5:11
     Multiple definitions for symbol: update
-    (at Cryptol:894:11--894:17, update)
+    (at Cryptol:899:11--899:17, update)
     (at ./T16/A.cry:3:1--3:7, T16::A::update)
diff --git a/tests/regression/safety.icry.stdout b/tests/regression/safety.icry.stdout
index 58fc9cb35..7313a61a3 100644
--- a/tests/regression/safety.icry.stdout
+++ b/tests/regression/safety.icry.stdout
@@ -3,7 +3,7 @@ Counterexample
 (\x -> assert x "asdf" "asdf") False ~> ERROR
 Run-time error: asdf
 -- Backtrace --
-Cryptol::error called at Cryptol:1048:41--1048:46
+Cryptol::error called at Cryptol:1053:41--1053:46
 Cryptol::assert called at safety.icry:3:14--3:20
 <interactive>::it called at safety.icry:3:7--3:37
 Counterexample
diff --git a/tests/regression/tc-errors.icry.stdout b/tests/regression/tc-errors.icry.stdout
index 5bdd30908..99e08fda9 100644
--- a/tests/regression/tc-errors.icry.stdout
+++ b/tests/regression/tc-errors.icry.stdout
@@ -83,19 +83,19 @@ Loading module Main
 
 [error] at tc-errors-5.cry:2:5--2:7:
   Inferred type is not sufficiently polymorphic.
-    Quantified variable: a`825
+    Quantified variable: a`826
     cannot match type: [0]?a
     When checking the type of 'Main::f'
   where
   ?a is type of sequence member at tc-errors-5.cry:2:5--2:7
-  a`825 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
+  a`826 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
 Loading module Cryptol
 Loading module Main
 
 [error] at tc-errors-6.cry:4:7--4:8:
   The type ?a is not sufficiently polymorphic.
-    It cannot depend on quantified variables: b`829
+    It cannot depend on quantified variables: b`830
     When checking the type of 'g'
   where
   ?a is the type of 'x' at tc-errors-6.cry:1:3--1:4
-  b`829 is signature variable 'b' at tc-errors-6.cry:3:8--3:9
+  b`830 is signature variable 'b' at tc-errors-6.cry:3:8--3:9