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