ajout issue54 corrigee

tests/sat/issue54.smt2

+(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)