Documentation

A simple variant of division, where we explicitly require the caller to make sure the divisor is not 0.

Check whether an arbitrary call to checkedDiv is safe. Clearly, we do not expect this to be safe:

>>> test1
[Documentation/SBV/Examples/Misc/NoDiv0.hs:38:14:checkedDiv: Divisor should not be 0: Violated. Model:
  s0 = 0 :: Int32
  s1 = 0 :: Int32]

Repeat the test, except this time we explicitly protect against the bad case. We have:

>>> test2
[Documentation/SBV/Examples/Misc/NoDiv0.hs:46:41:checkedDiv: Divisor should not be 0: No violations detected]