This is a repo for Software Verification Course.
This problem is from CodeForces (link: https://codeforces.com/contest/1646/problem/A)
squareCountProof.c contains the proof of the solution. This is to be run using cbmc. Running this with maxlen=16 works.
maxlen=16
cbmc -D N=$maxlen --unwind $(($maxlen + 2)) squareCountProof.c
However maxlen=32 does not terminate in a reasonable time.
maxlen=32
cbmc -D N=$maxlen --unwind $(($maxlen + 2)) squareCountProof.c
squareCountSol.c contains the solution to the problem.