From 798ef63598702de5363d32b49b0609c76b5ca65a Mon Sep 17 00:00:00 2001
From: Bruno Marre <bruno.marre@cea.fr>
Date: Wed, 23 Mar 2022 23:05:16 +0100
Subject: [PATCH] ajout issue54 corrigee

---
 tests/sat/issue54.smt2 | 24 ++++++++++++++++++++++++
 1 file changed, 24 insertions(+)
 create mode 100644 tests/sat/issue54.smt2

diff --git a/tests/sat/issue54.smt2 b/tests/sat/issue54.smt2
new file mode 100644
index 000000000..5fcad14c3
--- /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)
-- 
GitLab