solidity/test/libsolidity/smtCheckerTests/bmc_coverage/math_constructor.sol

mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
contract C {
	uint z = 1;
	uint w = z - 3;
}
// ====
// SMTEngine: bmc
// ----
// Warning 4144: (36-41): BMC: Underflow (resulting value less than 0) happens here.
[SMTChecker] Support check/unchecked 2020-12-16 17:32:34 +00:00			`contract C {`
			`uint z = 1;`
			`uint w = z - 3;`
			`}`
			`// ====`
			`// SMTEngine: bmc`
			`// ----`
Update old tests 2021-03-31 15:11:54 +00:00			`// Warning 4144: (36-41): BMC: Underflow (resulting value less than 0) happens here.`