Semantic discrepancy with division by zero (smt and mathematica)

[smover]

Mathematica and SMT adopt a different semantic for the division by zero, so we can get different verification results.

In SMT NRA the division is a partial function that is undetermined when the divisor is 0. So a/0 = b is true whatever is the value of a and b. This behavior is different for Mathematica, so we get different results.