diff --git a/lib/CryptolTC.z3 b/lib/CryptolTC.z3
index 59741bbe9..7d8736943 100644
--- a/lib/CryptolTC.z3
+++ b/lib/CryptolTC.z3
@@ -267,10 +267,12 @@
   ))
 )
 
-
-
 (declare-fun cryExpUnknown (Int Int) Int)
 
+(assert (forall ((x Int) (y Int))
+  (=> (and (> y 0) (> x 0))
+      (>= (cryExpUnknown x y) x))))
+
 (define-fun cryExpTable ((x Int) (y Int)) Int
   (ite (= y 0) 1
   (ite (= y 1) x
diff --git a/tests/issues/issue734.cry b/tests/issues/issue734.cry
new file mode 100644
index 000000000..69a506222
--- /dev/null
+++ b/tests/issues/issue734.cry
@@ -0,0 +1,8 @@
+f : {a} (fin a) => [2^^a - 1] -> [3*(2^^a - 1)]
+f x = x # x # x
+
+asdf1 : {r} (fin r, width (2^^r)==r+1) => [r+1]
+asdf1 = `(2^^r)
+
+asdf2 : {r} (fin r, width(2^^r-1)==r) => [r]
+asdf2 = `(2^^r-1)
diff --git a/tests/issues/issue734.icry b/tests/issues/issue734.icry
new file mode 100644
index 000000000..da54efefa
--- /dev/null
+++ b/tests/issues/issue734.icry
@@ -0,0 +1,6 @@
+:l issue734.cry
+
+f`{3} 0b1010101
+
+asdf1`{8}
+asdf2`{8}
diff --git a/tests/issues/issue734.icry.stdout b/tests/issues/issue734.icry.stdout
new file mode 100644
index 000000000..e47728b24
--- /dev/null
+++ b/tests/issues/issue734.icry.stdout
@@ -0,0 +1,6 @@
+Loading module Cryptol
+Loading module Cryptol
+Loading module Main
+0x156ad5
+0x100
+0xff