integer division (euclidein division)
node top(x, y:int)
z = x/y;
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.