Is there a function to perform euclidian integer division (like div from SMTLIB) in Sally? I can't seem to find one.
It looks like the / operator works on integers, but only if the division is exact, and otherwise things get in an inconsistent state where anything can be proved. This can be quite confusing, and it would be nicer if it was a type error to use / on an integer.
Is there a function to perform euclidian integer division (like
divfrom SMTLIB) in Sally? I can't seem to find one.It looks like the
/operator works on integers, but only if the division is exact, and otherwise things get in an inconsistent state where anything can be proved. This can be quite confusing, and it would be nicer if it was a type error to use/on an integer.