solidity/test/libsolidity/smtCheckerTests/array_members/push_zero_unsafe.sol

contract C {
	uint[] a;
	function f() public {
		a.push();
		assert(a[a.length - 1] == 100);
	}
}
// ====
// SMTEngine: all
// SMTIgnoreCex: no
// ----
// Warning 6328: (61-91): CHC: Assertion violation happens here.\nCounterexample:\na = [0]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()
// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
Add verification target for empty pop 2020-05-17 21:21:08 +00:00			`contract C {`
			`uint[] a;`
			`function f() public {`
			`a.push();`
			`assert(a[a.length - 1] == 100);`
			`}`
			`}`
Update old tests 2021-03-31 15:11:54 +00:00			`// ====`
			`// SMTEngine: all`
SMTChecker: Bring back counterexample checks in regression tests Since the default is now to ignore the counterexamples when checking test output, we bring back counterexample checks in tests where the counterexample is (mostly) deterministic. 2023-07-24 16:33:43 +00:00			`// SMTIgnoreCex: no`
Update test expectation 2020-05-18 14:33:27 +00:00			`// ----`
SMTChecker: Bring back counterexample checks in regression tests Since the default is now to ignore the counterexamples when checking test output, we bring back counterexample checks in tests where the counterexample is (mostly) deterministic. 2023-07-24 16:33:43 +00:00			`// Warning 6328: (61-91): CHC: Assertion violation happens here.\nCounterexample:\na = [0]\n\nTransaction trace:\nC.constructor()\nState: a = []\nC.f()`
Report safe properties in BMC and CHC 2023-02-09 16:07:13 +00:00			`// Info 1391: CHC: 2 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.`