1Warning: CHC: Underflow (resulting value less than 0) happens here. 2Counterexample: 3arr = [] 4a = 0x0 5x = 0 6 7Transaction trace: 8test.constructor() 9State: arr = [] 10test.f(0x0, 0) 11 --> model_checker_targets_all_chc/input.sol:7:3: 12 | 137 | --x; 14 | ^^^ 15 16Warning: CHC: Overflow (resulting value larger than 2**256 - 1) happens here. 17Counterexample: 18arr = [] 19a = 0x0 20x = 1 21 22Transaction trace: 23test.constructor() 24State: arr = [] 25test.f(0x0, 2) 26 --> model_checker_targets_all_chc/input.sol:8:3: 27 | 288 | x + type(uint).max; 29 | ^^^^^^^^^^^^^^^^^^ 30 31Warning: CHC: Division by zero happens here. 32Counterexample: 33arr = [] 34a = 0x0 35x = 0 36 37Transaction trace: 38test.constructor() 39State: arr = [] 40test.f(0x0, 1) 41 --> model_checker_targets_all_chc/input.sol:9:3: 42 | 439 | 2 / x; 44 | ^^^^^ 45 46Warning: CHC: Assertion violation happens here. 47Counterexample: 48arr = [] 49a = 0x0 50x = 0 51 52Transaction trace: 53test.constructor() 54State: arr = [] 55test.f(0x0, 1) 56 --> model_checker_targets_all_chc/input.sol:11:3: 57 | 5811 | assert(x > 0); 59 | ^^^^^^^^^^^^^ 60 61Warning: CHC: Empty array "pop" happens here. 62Counterexample: 63arr = [] 64a = 0x0 65x = 0 66 67Transaction trace: 68test.constructor() 69State: arr = [] 70test.f(0x0, 1) 71 --> model_checker_targets_all_chc/input.sol:12:3: 72 | 7312 | arr.pop(); 74 | ^^^^^^^^^ 75 76Warning: CHC: Out of bounds access happens here. 77Counterexample: 78arr = [] 79a = 0x0 80x = 0 81 82Transaction trace: 83test.constructor() 84State: arr = [] 85test.f(0x0, 1) 86 --> model_checker_targets_all_chc/input.sol:13:3: 87 | 8813 | arr[x]; 89 | ^^^^^^ 90