cbmc doesn't execute C(++) programs, but rather it turns them into instances of the SAT problem, which it then passes off to a SAT prover to (hopefully) prove i

cbmc doesn't execute C(++) programs, but rather it turns them into instances of the SAT problem, which it then passes off to a SAT prover to (hopefully) prove it. It's assert() (and assume() and nondet_xxx() which are not mentioned in the article) that have special powers in cbmc, but functions name prove_xxx() aren't special as far as I'm aware.