With working directory as src/test/cbmc/LoopLoop_NonReturning:
The following works fine:
rmc main.rs --cbmc-args --unwind 10
The following does not terminate:
rmc --visualize main.rs --cbmc-args --unwind 10
When I manually set cover_args to ["--unwind", "10"], it terminates successfully.
Possible solution: add --unwind as an RMC flag, and if present, add it to cover_args as well.
With working directory as
src/test/cbmc/LoopLoop_NonReturning:The following works fine:
rmc main.rs --cbmc-args --unwind 10The following does not terminate:
rmc --visualize main.rs --cbmc-args --unwind 10When I manually set
cover_argsto["--unwind", "10"], it terminates successfully.Possible solution: add
--unwindas an RMC flag, and if present, add it tocover_argsas well.