\myheading{School-level equation: CBMC}

Doing this again with CBMC:

\lstinputlisting[style=customc]{equations/CBMC_eq/eq1.c}

\begin{lstlisting}
% cbmc --trace --function main eq1.c

...
** Results:
eq1.c function main
[main.assertion.1] line 15 assertion 0: FAILURE

Trace for main.assertion.1:

State 21 file eq1.c function main line 5 thread 0
----------------------------------------------------
  circle=5 (00000000 00000000 00000000 00000101)

State 22 file eq1.c function main line 5 thread 0
----------------------------------------------------
  square=-2147483646 (10000000 00000000 00000000 00000010)

State 23 file eq1.c function main line 5 thread 0
----------------------------------------------------
  triangle=-2147483647 (10000000 00000000 00000000 00000001)
...
\end{lstlisting}

Ouch! This is correct solution, but for signed integers.

I can fix it:

\lstinputlisting[style=customc]{equations/CBMC_eq/eq2.c}

\begin{lstlisting}
 % cbmc --trace --function main eq2.c

...

** Results:
eq2.c function main
[main.assertion.1] line 21 assertion 0: FAILURE

Trace for main.assertion.1:

State 21 file eq2.c function main line 5 thread 0
----------------------------------------------------
  circle=5 (00000000 00000000 00000000 00000101)

State 22 file eq2.c function main line 5 thread 0
----------------------------------------------------
  square=2 (00000000 00000000 00000000 00000010)

State 23 file eq2.c function main line 5 thread 0
----------------------------------------------------
  triangle=1 (00000000 00000000 00000000 00000001)

...
\end{lstlisting}

Or let's just declare unsigned integers, this will also work:

\lstinputlisting[style=customc]{equations/CBMC_eq/eq3.c}

CBMC can also export SMT-LIB 2 file:

\begin{lstlisting}
% cbmc --trace --function main --smt2 --outfile 1.smt eq3.c
\end{lstlisting}

The core of it is:

\lstinputlisting[style=customsmt]{equations/CBMC_eq/1.smt_part}

(Full version: \url{\RepoURL/equations/CBMC_eq/1.smt}.)

I can run it separately in SMT solver:

\lstinputlisting[style=customsmt]{equations/CBMC_eq/1.txt}

This is the correct solution indeed.