[SAL-HELP] Iterative counterexamples?

[Lee Pike]

Hello,

I'd like to use SAL (either sal-bmc or sal-smc) to generate all the  
counterexamples (or up to some finite limit of counterexamples) to a  
state invariant over a finite model.

I'm writing to see if there's a known option to do so, or if someone  
knows how this can easily be done.

Thanks,
Lee

--
Galois, Inc.
<http://www.galois.com>
<http://www.galois.com/company/people/lee_pike>

Phone: +1 503.626.6616 ext. 135
Fax: +1 503.350.0833