Skip to content
Snippets Groups Projects
user avatar
Jan Rochel authored
The occurrence of rationals in the following logic function lead to an
assertion failure in Interval_utils.extract_ival, which was only defined
for non-integer arguments.

/*@
    logic integer signum(ℝ x) =
      x > 0. ? 1 : x < 0. ? -1 : 0;
*/

Regression test added: src/plugins/e-acsl/tests/arith/sign_rational.c
a5caf8c1
History
user avatar a5caf8c1
Name Last commit Last update