11. The apparatus of claim 10 , wherein the bounded model checker further includes a proof generator in communication with the arithmetic satisfiability solver, the proof generator to output a proof of unsatisfiability in the case where the one or more numeric formulas generated by the bounded model checker are collectively unsatisfiable.
10. The apparatus of claim 9 , wherein the bounded model checker further includes an arithmetic satisfiability solver to search for a numeric assignment of numbers to variables in the one or more numeric formulas generated by the bounded model checker to find a solution to the numeric formulas.