Adding tests and updating handling of zero_extend 0

OCamlPro · Sep 26, 2023 · 570af3f · 570af3f
1 parent e1df59f
commit 570af3f
Show file tree

Hide file tree

Showing 2 changed files with 22 additions and 0 deletions.
diff --git a/src/lib/reasoners/bitv.ml b/src/lib/reasoners/bitv.ml
@@ -213,6 +213,8 @@ module Shostak(X : ALIEN) = struct
         { descr = Vextract (t', i, j); size }
       | { f = Op BVnot; xs = [ t ]; ty = Tbitv size; _ } ->
         { descr = Vnot t; size }
+      | { f = Op BVZeroExtend n; xs = [ t ]; ty = Tbitv size; _ } when n = 0 ->
+        { descr = Vother t; size }
       | { f = Op BVZeroExtend n; xs = [ t ]; ty = Tbitv size; _ } when n > 0 ->
         { descr = Vconcat (E.BV.bvzero n, t); size = n + size }
       | { ty = Tbitv size; _ } ->

diff --git a/tests/dune.inc b/tests/dune.inc