bound_texpr could be more precise for non-linear expressions

[rmonat]

Following a discussion with @jboillot in the Mopsa static analyzer, I believe bound_texpr could be more precise. Consider the case where x >= y and z >= 0. Currently, bound_texpr on (x-y)*z returns [-oo,+oo], while it could return [0, +oo].

I tried bound_texpr on x-y, the result is precise. I also tried bounding x*y when x >= 0, y >= 0, and got a precise result.

Code to reproduce the issue:

open Apron

let man = Polka.manager_alloc_loose ()
let env = Environment.make (Array.map Var.of_string [|"x"; "y"; "z"|]) [||]
let top = Abstract1.top man env
let tv s = Texpr1.var env (Var.of_string s)
let cons1 = Tcons1.make (tv "z") SUPEQ
let cons2 = Tcons1.make (Texpr1.binop Sub
                           (tv "x")
                           (tv "y")
                           Int Rnd) SUPEQ
let cons = Tcons1.array_make env 2
let () = Tcons1.array_set cons 0 cons1
let () = Tcons1.array_set cons 1 cons2
let a = Abstract1.meet_tcons_array man top cons
let () = Tcons1.array_print Format.std_formatter (Abstract1.to_tcons_array man a)
let xmy = Texpr1.binop Sub (tv "x") (tv "y") Int Rnd
let e = Texpr1.binop Mul xmy (tv "z") Int Rnd
let itv = Abstract1.bound_texpr man a e
let () = Format.printf "@.%a in %a@." Texpr1.print e Interval.print itv 

Tried with apron 0.9.13, 0.9.14, using either the Polka or Octagon domain.