1. A method for circuit verification using multiple engines, the method comprising: running a plurality of traces on a circuit using a plurality of reachability algorithms; selecting an effective reachability algorithm for the circuit from among the plurality of reachability algorithms according to a comparison of results of the plurality of traces with each other; generating a set of initial states for the selected effective reachability algorithm using states reached in the plurality of traces; and executing the selected effective reachability algorithm using the generated set of initial states to verify the circuit.