Switch to accurate bounds for lor

When the arguments are, e.g., 2^k - 2 and 2^(k-1)-1, the upper bound is 2^k - 1, not 2^(k-1)-1.

Thanks, Rob

1 files changed, 1 insertions, 1 deletions

diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v
index 0da74da09..cfdd8bd08 100644
--- a/src/Reflection/Z/Interpretations.v
+++ b/src/Reflection/Z/Interpretations.v
@@ -351,7 +351,7 @@ Module ZBounds.
   Definition lor' : bounds -> bounds -> bounds
     := fun x y => let (lx, ux) := x in let (ly, uy) := y in
                                        {| lower := Z.max lx ly;
-                                          upper := 2^(Z.max (Z.log2 (ux+1)) (Z.log2 (uy+1))) - 1 |}.
+                                          upper := 2^(Z.max (Z.log2_up (ux+1)) (Z.log2_up (uy+1))) - 1 |}.
   Definition lor : t -> t -> t := t_map2 lor'.
   Definition neg' : bounds -> bounds -> bounds
     := fun int_width v