From 1a419ffbff45d7d0d4c8aeb22cd043726c41c197 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?L=C3=A9on=20Frenot?= <leon.frenot@ens-lyon.fr>
Date: Mon, 25 Nov 2024 14:27:24 +0000
Subject: [PATCH] Added back Eq and Ne tests cases

---
 test/lean/bitvec_operation.expected.lean |  6 ++++++
 test/lean/bitvec_operation.sail          | 10 ++++++++++
 2 files changed, 16 insertions(+)

diff --git a/test/lean/bitvec_operation.expected.lean b/test/lean/bitvec_operation.expected.lean
index 24d4d1b90..7e2d7f2e7 100644
--- a/test/lean/bitvec_operation.expected.lean
+++ b/test/lean/bitvec_operation.expected.lean
@@ -1,3 +1,9 @@
+def bitvector_eq (x : BitVec 16) (y : BitVec 16) : Bool :=
+  (Eq x y)
+
+def bitvector_neq (x : BitVec 16) (y : BitVec 16) : Bool :=
+  (Ne x y)
+
 def bitvector_append (x : BitVec 16) (y : BitVec 16) : BitVec 32 :=
   (BitVec.append x y)
 
diff --git a/test/lean/bitvec_operation.sail b/test/lean/bitvec_operation.sail
index 24de92c3e..a8b6861cb 100644
--- a/test/lean/bitvec_operation.sail
+++ b/test/lean/bitvec_operation.sail
@@ -2,6 +2,16 @@ default Order dec
 
 $include <prelude.sail>
 
+val bitvector_eq : (bits(16), bits(16)) -> bool
+function bitvector_eq(x, y) = {
+  x == y
+}
+
+val bitvector_neq : (bits(16), bits(16)) -> bool
+function bitvector_neq(x, y) = {
+  x != y
+}
+
 val bitvector_append : (bits(16), bits(16)) -> bits(32)
 function bitvector_append(x, y) = {
   append (x, y)