# BMC: no counterexample found of length up to 5
# BMC: formula failed
# BMC: formula failed
# BMC: formula failed