Open rmonat opened 4 months ago
In an email exchange with @GgnDpSngh highlighted that NewPolka with 64-bit integers does not seem to terminate in this case. Explanations about Elina's behavior:
The cause for issue #96 is due to the fact the constraint that you pass gets converted into x+9223372036854775808>=0. 9223372036854775808 encoded as MPQ in initial tcons is ultimately converted into int64 (the datatype used for Polyhedra in ELINA) using the call at https://github.com/eth-sri/ELINA/blob/f524156d292ac3a6f3cd676e2d2e7db6629e2b6f/elina_linearize/elina_int.h#L79. Since 9223372036854775808 cannot be represented as int64, mpz_get_si returns 0 and instead of adding x+9223372036854775808>=0, we add x>=0. The intersection of this with the second constraint you pass is empty. This is also an unavoidable error unless mpz_get_si has some form of error detection that I can propagate through.
I have an edge case were adding constraint
x - (-9223372036854775808) >= 0
and then adding constraint-9223372036854775808 - x >= 0
yields bottom for elina_poly, which is unsound. Would there be an easy way to fix this issue?MWE:
Output (with the unexpected bottom for elina_poly):