seahorn/crab

Bug with apron-domains and rationals

caballa opened this issue · 0 comments

From @caballa on February 16, 2017 21:22

Added test case in branch crab2 (commit 9a21877) that triggers the bug.
The test is actually quite simple. If we just add two constraints x >= 1/2 and x <= 1/2 we get bottom rather than x = 1/2.

If we use integers we get the expected result so something is wrong with how we handle rationals.

Copied from original issue: caballa/crab#12