SE547: CBMC: CBMC Algorithm [12/19]

6) Hand off checking C P to a SAT-solver.

Solving with ZChaff version ZChaff 2003.6.16
1222 variables, 3948 clauses
SAT checker: negated claim is UNSATISFIABLE, i.e., holds
VERIFICATION SUCCESSFUL

We talked about SAT-solvers last week.