solidity/test/libsolidity/smtCheckerTests/invariants/loop_basic.sol

pragma experimental SMTChecker;

contract Simple {
	function f(uint x) public pure {
		uint y;
		require(x > 0);
		while (y < x)
			++y;
		assert(y == x);
	}
}
// ====
// SMTSolvers: z3
// ----
[SMTChecker] Add loop support 2019-08-20 13:03:45 +00:00			`pragma experimental SMTChecker;`

			`contract Simple {`
			`function f(uint x) public pure {`
			`uint y;`
			`require(x > 0);`
			`while (y < x)`
			`++y;`
			`assert(y == x);`
			`}`
			`}`
Set tests that CVC4 can't handle to Z3 only 2019-12-04 15:39:34 +00:00			`// ====`
			`// SMTSolvers: z3`
[SMTChecker] Adding unary increment and decrement as under/overflow verification targets for the CHC engine 2020-12-10 15:51:10 +00:00			`// ----`