% generated by paper/tools/contexts.py from the ctx-mutual-* claims
\begin{tabular}{@{}lrllll@{}}
\toprule
Context policy & Contexts & \multicolumn{2}{l}{\texttt{res1 == 2}} & \multicolumn{2}{l}{\texttt{res2 == 1}} \\
\midrule
one context per procedure & 2 & \verdict{UNKNOWN} & $[1,12]$ & \verdict{UNKNOWN} & $[1,12]$ \\
call strings, length 1 & 4 & \verdict{UNKNOWN} & $[1,12]$ & \verdict{UNKNOWN} & $[1,12]$ \\
call strings, length 2 & 6 & \verdict{PROVED} & $[2,2]$ & \verdict{PROVED} & $[1,1]$ \\
entry states & 6 & \verdict{PROVED} & $[2,2]$ & \verdict{PROVED} & $[1,1]$ \\
\bottomrule
\end{tabular}