\myheading{Least Common Multiple}

To find LCM of 4 and 6, we are going to solve the following diophantine (i.e., allowing only integer solutions) system of equations:

$4x = 6y = LCM$

... where LCM>0 and as small, as possible.

\begin{lstlisting}
#!/usr/bin/env python

from z3 import *

opt = Optimize()

x,y,LCM=Ints('x y LCM')

opt.add(x*4==LCM)
opt.add(y*6==LCM)
opt.add(LCM>0)

h=opt.minimize(LCM)

print (opt.check())
print (opt.model())
\end{lstlisting}

The (correct) answer:

\begin{lstlisting}
sat
[y = 2, x = 3, LCM = 12]
\end{lstlisting}