  Our recently proposed certification framework for bit-level k-induction-based
model checking has been shown to be quite effective in increasing the trust of
verification results even though it partially involved quantifier reasoning. In
this paper we show how to simplify the approach by assuming reset functions to
be stratified. This way it can be lifted to word-level and in principle to
other theories where quantifier reasoning is difficult. Our new method requires
six simple SAT checks and one polynomial-time check, allowing certification to
remain in co-NP while the previous approach required five SAT checks and one
QBF check. Experimental results show a substantial performance gain for our new
approach. Finally, we present and evaluate our new tool Certifaiger-wl which is
able to certify k-induction-based word-level model checking.
