Octagon overflow during assignment not handled correctly?

[rmonat]

I tested an assignment creating an overflow in Elina's internal representation, starting from top. The polyhedra domain signals an overflows and returns top. However, the octagon domain does not appear to signal the overflow, and returns bottom, which is unsound. I tested all this through the apron interface (apron v0.9.14, elina v1.3.2 through opam).

Can this be easily fixed?

MWE:

open Apron

let test_assign name man =
  let env = Environment.make (Array.map Var.of_string [|"x"; "y"; "z"|]) [||] in
  let top = Abstract1.top man env in 
  let e = Texpr1.binop Sub 
      (Texpr1.unop Neg (Texpr1.cst env (Coeff.s_of_mpq (Mpq.of_string "9223372036854775807")))  Int Rnd)
      (Texpr1.cst env (Coeff.s_of_int 1))
      Int Rnd in
  let a = Abstract1.assign_texpr man top (Apron.Var.of_string "x") e None in 
  Format.printf "[%s] after x = %a, a = %a@." name Texpr1.print e Abstract1.print a

let () = test_assign "elina_poly" (Elina_poly.manager_alloc_loose ())
let () = test_assign "elina_oct" (Elina_oct.manager_alloc ())
let () = test_assign "apron_oct" (Oct.manager_alloc ())
let () = test_assign "apron_poly" (Polka.manager_alloc_loose ())

$ dune exec elina_issue
overflow exception                 
[elina_poly] after x = -9223372036854775807 -_i,? 1, a = top
[elina_oct] after x = -9223372036854775807 -_i,? 1, a = bottom
[apron_oct] after x = -9223372036854775807 -_i,? 1, a = [|x
                                                          +9223372036854775808>=0;
                                                          -x
                                                          -9223372036854775808>=0|]
[apron_poly] after x = -9223372036854775807 -_i,? 1, a = [|x
                                                           +9223372036854775808=0|]

Thank you!

EDIT: I just realized Elina v1.3.2 might be outdated (although it's the latest version available on opam). I'm still obtaining the results on latest version (commit f524156d292ac3a6f3cd676e2d2e7db6629e2b6f)

[rmonat]

In an email exchange, @GgnDpSngh indicated the octagon domain in Elina is designed to work with doubles. In particular, changing the Texpr1.typ from Int to Double fixes this issue.