Bug #65
closedinteger division (euclidein division)
Start date:
05/08/2018
Due date:
% Done:
0%
Estimated time:
Description
node top(x, y:int)
returns(z:int);
let
z = x/y;
tel
This is translated as x/y in C, which is different from Simulink coder approch (verifying the sign of numerator and denominator).
top(-4, 3) Simulink/Kind2 is giving -2 and Lustrec is giving -1.
-4 = 3*(-2) + 2; or -4 = 3*(-1) -1;
I think the modulo should be positive. So I go with Simulink/Kind2 result.
Updated by Pierre-Loïc Garoche over 3 years ago
Considering producing valid integer division and modulo instead of C ones. To be discussed.
Updated by Hamza Bourbouh over 3 years ago
- Status changed from New to Closed
Solved in unstable branch