Example 4.10 / Appendix A - Inductive behavior in BMC

The SMV model described in Example 4.10 and printed in Appendix A consists of a 3-bit counter x, and a 4-bit counter y. It was generated by the bash shell script induction_example.sh. The script takes one parameter 'n', and will generate an SMV model for any n-bit counter x and (n+1)-bit counter y.

The SMV model was subsequently translated to AIGER format using the tool smvtoaig, which can be found in the AIGER 1.9.4 toolset.

The resulting AIGER benchmark was solved using the modified version of AIGBMC.