feat(sby_engine_aiger): add rIC3 support for BMC mode

[SeddonShen]

What are the reasons/motivation for this change?

• This change extends the functionality of the rIC3 solver in the sby_engine_aiger.py module to support BMC mode. Previously, rIC3 was only supported in prove mode, which limited its use cases.

Explain how this is achieved.

• the ric3 solver command is configured with specific BMC-related arguments, such as --bmc-max-k to define the maximum depth and -e bmc to enable BMC mode. Additionally, a status_2 variable is introduced to handle the BMC pass status output by rIC3.

If applicable, please suggest to reviewers how they can test the change.

1. Running a BMC task using the rIC3 solver in a test environment.
2. Verifying that the solver correctly executes in BMC mode and produces the expected results.
3. Ensuring that the existing prove mode functionality remains unaffected.