added time for z4 problem 4

[ar1516.git] / a2 / 4.tex

diff --git a/a2/4.tex b/a2/4.tex
index b1e6641..81f3cd5 100644 (file)
--- a/a2/4.tex
+++ b/a2/4.tex
@@ -107,8 +107,8 @@ $$\mathcal{INIT}\wedge\left(\bigwedge_{i=1}^{31}\mathcal{ITER}(i)\right)
 \subsection{Solution}
 The conversion to SMT-Lib is trivial however on a $3.8Ghz$ processor running
 \textsc{yices} it takes about $4$ hours and $15$ minutes to find the solution
-listed in Table~\ref{tab:sol}.
-
+listed in Table~\ref{tab:sol}. \textsc{z3} finds a solution in $10$ minutes and
+$37$ seconds.
 
 \begin{table}[h]
        \centering