Added back Eq and Ne tests cases

rems-project · Nov 25, 2024 · 1a419ff · 1a419ff
1 parent 44e3256
commit 1a419ff
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 0 deletions.
diff --git 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
@@ -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)