solidity/test/cmdlineTests/model_checker_invariants_contract_reentrancy/input.sol

// SPDX-License-Identifier: GPL-3.0
pragma solidity >=0.0;
contract test {
	uint x;
    function f(address _a) public {
		_a.call("");
		assert(x == 0);
    }
}