Fixes test

formalsec · Feb 18, 2024 · 141c751 · 141c751
1 parent 2e54af2
commit 141c751
Show file tree

Hide file tree

Showing 2 changed files with 1 addition and 3 deletions.
diff --git a/test/unit/test_bitv8.ml b/test/unit/test_bitv8.ml
@@ -8,4 +8,4 @@ let () =
   let x = I8.sym "x" in
   assert (Z3.check solver [ I8.(x > v 0) ]);
   let v = Z3.get_value solver x in
-  assert (v.node.e = Val (Num (I8 1)))
+  assert (v >= I8.v 1)
diff --git a/test/unit/test_normalization.ml b/test/unit/test_normalization.ml
@@ -6,6 +6,4 @@ let () =
   let y = Bitv.I32.sym "y" in
   let e1 = Bitv.I32.(x > y) in
   let e2 = Bitv.I32.(y < x) in
-  Format.printf "e1: %[email protected]: %a@." pp e1 pp e2;
-  (* Hash-consing not working?! *)
   assert (e1 == e2)