diff --git a/tests/issues/T146.icry.stdout b/tests/issues/T146.icry.stdout
index cdb8f7c9..751b8bb6 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`772
+    It cannot depend on quantified variables: fv`775
     When checking type of field 'v0'
   where
   ?a is type argument 'fv' of 'Main::ec_v1' at T146.cry:4:19--4:24
-  fv`772 is signature variable 'fv' at T146.cry:11:10--11:12
+  fv`775 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`772
+    It cannot depend on quantified variables: fv`775
     When checking signature variable 'fv'
   where
   ?b is type argument 'fv' of 'Main::ec_v2' at T146.cry:5:19--5:24
-  fv`772 is signature variable 'fv' at T146.cry:11:10--11:12
+  fv`775 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 cf4cc227..c559296e 100644
--- a/tests/issues/issue1024.icry.stdout
+++ b/tests/issues/issue1024.icry.stdout
@@ -8,20 +8,20 @@ Loading module Main
 [warning] at issue1024a.cry:4:34--4:39 Unused name: g
 
 [error] at issue1024a.cry:1:6--1:11:
-  Illegal kind assigned to type variable: f`769
-  Unexpected: # -> *
-  where
-  f`769 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`770
-  Unexpected: Prop
-  where
-  f`770 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`772
   Unexpected: # -> *
   where
-  f`772 is signature variable 'f' at issue1024a.cry:4:22--4:32
+  f`772 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`773
+  Unexpected: Prop
+  where
+  f`773 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`775
+  Unexpected: # -> *
+  where
+  f`775 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 f68886c0..92d90681 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:951:13--951:18
+Cryptol::error called at Cryptol:967:13--967: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 b1d3ce75..9b189b24 100644
--- a/tests/issues/issue226.icry.stdout
+++ b/tests/issues/issue226.icry.stdout
@@ -51,6 +51,7 @@ Primitive Types
     Integral : * -> Prop
     inf : #
     Literal : # -> * -> Prop
+    LiteralLessThan : # -> * -> Prop
     Logic : * -> Prop
     lengthFromThenTo : # -> # -> # -> #
     max : # -> # -> #
@@ -145,10 +146,13 @@ Symbols
       {first, last, a} (fin last, last >= first, Literal first a,
                         Literal last a) =>
         [1 + (last - first)]a
+    fromToLessThan :
+      {first, bound, a} (fin first, bound >= first,
+                         LiteralLessThan bound a) =>
+        [bound - first]a
     fromZ : {n} (fin n, n >= 1) => Z n -> Integer
     generate :
-      {n, a, ix} (fin n, n >= 1, Integral ix, Literal (n - 1) ix) =>
-        (ix -> a) -> [n]a
+      {n, a, ix} (Integral ix, LiteralLessThan n ix) => (ix -> a) -> [n]a
     groupBy :
       {each, parts, a} (fin each) => [each * parts]a -> [parts][each]a
     head : {n, a} [1 + n]a -> a
diff --git a/tests/issues/issue290v2.icry.stdout b/tests/issues/issue290v2.icry.stdout
index e30dc46e..b851535a 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`769 == 1
+    • n`772 == 1
         arising from
         checking a pattern: type of 1st argument of Main::minMax
         at issue290v2.cry:2:8--2:11
   where
-  n`769 is signature variable 'n' at issue290v2.cry:1:11--1:12
+  n`772 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 883d7c76..1b328458 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`769
+        • k == n`772
             arising from
             matching types
             at issue723.cry:7:17--7:19
   where
-  n`769 is signature variable 'n' at issue723.cry:1:6--1:7
+  n`772 is signature variable 'n' at issue723.cry:1:6--1:7
diff --git a/tests/issues/issue848.icry.stdout b/tests/issues/issue848.icry.stdout
index 1f3ada03..7e23d079 100644
--- a/tests/issues/issue848.icry.stdout
+++ b/tests/issues/issue848.icry.stdout
@@ -1,6 +1,4 @@
 Loading module Cryptol
-a : {n, a} (Integral a, n >= 1, Literal (max 10 (n - 1)) a,
-            fin n) =>
-      [n]a
+a : {n, a} (Integral a, LiteralLessThan n a, Literal 10 a) => [n]a
 [0x0000000a, 0x0000000b, 0x0000000c, 0x0000000d, 0x0000000e,
  0x0000000f, 0x00000010, 0x00000011, 0x00000012, 0x00000013]
diff --git a/tests/regression/safety.icry.stdout b/tests/regression/safety.icry.stdout
index 800bcc60..c93549fe 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:959:41--959:46
+Cryptol::error called at Cryptol:975:41--975: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 2c5dc64f..e2560fcc 100644
--- a/tests/regression/tc-errors.icry.stdout
+++ b/tests/regression/tc-errors.icry.stdout
@@ -84,19 +84,19 @@ Loading module Main
 
 [error] at tc-errors-5.cry:2:5--2:7:
   Inferred type is not sufficiently polymorphic.
-    Quantified variable: a`769
+    Quantified variable: a`772
     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`769 is signature variable 'a' at tc-errors-5.cry:1:6--1:7
+  a`772 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`773
+    It cannot depend on quantified variables: b`776
     When checking the type of 'Main::g'
   where
   ?a is the type of 'x' at tc-errors-6.cry:1:3--1:4
-  b`773 is signature variable 'b' at tc-errors-6.cry:3:8--3:9
+  b`776 is signature variable 'b' at tc-errors-6.cry:3:8--3:9