\myheading{Division by 0}

How SMT-solvers handles division by zero?
They can't throw exception, like a CPU.

It was decided to \textit{totalize} division operation, i.e., make it producing an output for each input.
But which output should be for $\frac{x}{0}$?

One idea was that $\frac{x}{0}$ should be 0, as this is 
\href{https://cs.nyu.edu/pipermail/smt-lib/2015/000977.html}{done} in theorem-provers.

Another idea is to fix $\frac{x}{0}$ to \verb|0b11...11| or \verb|0xff..ff|:

\begin{lstlisting}
From an implementation point of view, the simplest approach is one that
avoids special treatments for division by zero and makes things uniform.

The majority of implementers have chosen (bvudiv x 0) = 11...1 because
that's what you get from a long division algorithm or divider circuit
based on long division, and I guess that's how most of us implement division
in SMT solvers.

It is also reasonable to define:

     (bvurem x y) = x - (bvudiv x y) * y.

This equality is already required by SMT-LIB when y>0. If we require
the equality to also hold for y=0, we have  (bvurem x 0) = x no matter
how we define (bvudiv x 0). This is again consistent with what the
long-division algorithm produces.
\end{lstlisting}
( \href{https://cs.nyu.edu/pipermail/smt-lib/2017/001163.html}{src} )

This is quite fun, I tried to divide by zero using my toy-blaster MK85,
this resulted in \verb|0xff..ff|, since my solver implements a primitive divisor.

See also, \href{https://cs.nyu.edu/pipermail/smt-lib/2017/001148.html}{start of discussion}.

From the \href{https://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml}{SMT-LIB standard}:

\begin{lstlisting}
   [[(bvudiv s t)]] := if bv2nat([[t]]) = 0
                       then λx:[0, m). 1
                       else nat2bv[m](bv2nat([[s]]) div bv2nat([[t]]))


...

 "After extensive discussion, it was decided to fix the value of
   (bvudiv s t) and (bvurem s t) in the case when bv2nat([[t]]) is 0.
   While this solution is not preferred by all users, it has the
   advantage that it simplifies solver implementations.  Furthermore,
   it is straightforward for users to use alternative semantics by
   defining their own version of these operators (using define-fun) and
   using ite to insert their own semantics when the second operand is
   0.
 "
\end{lstlisting}

If you want to \textit{disable} division by zero, you can still add a constraint preventing divisor to be zero.
And if your equation would \textit{require} to divide by 0, you'll get \textit{unsat}.

Anyway, you can always add an \ac{ITE}, that will branch depending on the value of divisor.