Warning: BMC: Assertion violation happens here. --> model_checker_engine_bmc/input.sol:5:3: | 5 | assert(x > 0); | ^^^^^^^^^^^^^ Note: Counterexample: x = 0 Note: Callstack: Note: