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

contract C {
	struct S {
		int[] b;
	}
	S s;
	struct T {
		S s;
	}
	T t;
	function f() public {
		s.b.push() = t.s.b.push();
		assert(s.b[s.b.length -1] == t.s.b[t.s.b.length - 1]);
	}
}
// ====
// SMTEngine: all
// ----
// Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.
[SMTChecker] Fix internal error when array.push() is used as LHS of assignment 2020-10-26 16:16:27 +00:00			`contract C {`
			`struct S {`
			`int[] b;`
			`}`
			`S s;`
			`struct T {`
			`S s;`
			`}`
			`T t;`
			`function f() public {`
			`s.b.push() = t.s.b.push();`
			`assert(s.b[s.b.length -1] == t.s.b[t.s.b.length - 1]);`
			`}`
			`}`
Update old tests 2021-03-31 15:11:54 +00:00			`// ====`
Trivial isoltest updates: normalized whitespace 2021-03-12 23:02:36 +00:00			`// SMTEngine: all`
Trivial isoltest updates: missing // ---- at the end 2021-03-12 23:02:36 +00:00			`// ----`
Report safe properties in BMC and CHC 2023-02-09 16:07:13 +00:00			`// Info 1391: CHC: 5 verification condition(s) proved safe! Enable the model checker option "show proved safe" to see all of them.`