14. A system according to claim 1 wherein said model checking engine, after said evaluation of said assertions over said subset, is responsive to said ICUT-based trace to generate a new initial state, apply said new initial state to said basic logic, evaluate said assertion over a new subset of said states reachable from said new initial state.
15. A system according to claim 14 wherein said model checker engine includes means determining whether a model checker-based trace is a reproduction of said ICUT-based trace.