Warning: CHC: Assertion violation happens here. Counterexample: x = 0 Transaction trace: B.constructor() B.f(0) --> model_checker_contracts_all_explicit/input.sol:5:3: | 5 | assert(x > 0); | ^^^^^^^^^^^^^ Warning: CHC: Assertion violation happens here. Counterexample: y = 0 Transaction trace: A.constructor() A.g(0) --> model_checker_contracts_all_explicit/input.sol:10:3: | 10 | assert(y > 0); | ^^^^^^^^^^^^^