Warning: BMC: Condition is always true.
 --> model_checker_targets_constant_condition_bmc/input.sol:7:11:
  |
7 | 		require(x >= 0);
  | 		        ^^^^^^
Note: Callstack: