diff --git a/tests/sat/issue54.smt2 b/tests/sat/issue54.smt2
new file mode 100644
index 0000000000000000000000000000000000000000..5fcad14c3ffb907a618f2ce2cf3644f648741627
--- /dev/null
+++ b/tests/sat/issue54.smt2
@@ -0,0 +1,24 @@
+(set-logic ALL)
+(set-info :smt-lib-version 2.6)
+(set-info :status sat)
+
+(define-fun uint_in_range ((i Int)) Bool
+  (and (<= 0 i) (<= i 18446744073709551615)))
+
+(declare-sort t 0)
+
+(declare-fun first (t) (_ BitVec 64))
+(declare-fun last (t) (_ BitVec 64))
+
+(define-fun t2_length ((a1 t)) Int
+  (ite (bvule (first a1) (last a1))
+    (+ (- (bv2nat (last a1)) (bv2nat (first a1))) 1)
+    0))
+
+(declare-const c t)
+
+(assert (and (= (first c) #x0000000000000000) (= (last c) #xFFFFFFFFFFFFFFFF)))
+
+(assert (not (uint_in_range (t2_length c))))
+
+(check-sat)