JKind does not detect division by zero (using / or 'div'). Instead, it relies on the behavior of the underlying solver which is probably inconsistent and may result in error messages directly from the solver.
Since you can only divide by constants, we should be able to detect this statically. However, doing the detection requires writing code for evaluation of expression which is more work than I'm willing to do at the moment.
JKind does not detect division by zero (using / or 'div'). Instead, it relies on the behavior of the underlying solver which is probably inconsistent and may result in error messages directly from the solver.
Since you can only divide by constants, we should be able to detect this statically. However, doing the detection requires writing code for evaluation of expression which is more work than I'm willing to do at the moment.
Thanks to Lucas Wagner for pointing this out.