diff options
Diffstat (limited to 'abstract/intervals_domain.ml')
| -rw-r--r-- | abstract/intervals_domain.ml | 9 |
1 files changed, 2 insertions, 7 deletions
diff --git a/abstract/intervals_domain.ml b/abstract/intervals_domain.ml index d95a938..06c5e57 100644 --- a/abstract/intervals_domain.ml +++ b/abstract/intervals_domain.ml @@ -43,10 +43,8 @@ module Intervals : VALUE_DOMAIN = struct if i < Z.zero then PInf else MInf | Int i, Int j -> - if j = Z.zero then - if i < Z.zero then MInf - else PInf - else Int (Z.div i j) + assert (j != Z.zero); + Int (Z.div i j) let bound_min a b = match a, b with @@ -116,8 +114,6 @@ module Intervals : VALUE_DOMAIN = struct (bound_min (bound_mul b c) (bound_mul b d))), (bound_max (bound_max (bound_mul a c) (bound_mul a d)) (bound_max (bound_mul b c) (bound_mul b d)))) - - let div a b = match a, b with | Bot, _ -> Bot | Itv(a, b), q -> @@ -132,7 +128,6 @@ module Intervals : VALUE_DOMAIN = struct Itv(min (bound_div b c) (bound_div b d), max (bound_div a c) (bound_div a d)) in join p1 p2 - let rem a b = match a, b with | Bot, _ | _, Bot -> Bot | Itv(a, b), Itv(c, d) -> |