solidity/test/libsolidity/smtCheckerTests/types/mapping_4.sol

mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
pragma experimental SMTChecker;

contract C
{
	mapping (bool => bool) map;
	function f(bool x) public view {
		require(x);
		assert(x != map[x]);
	}
}
// ====
// SMTSolvers: z3
[SMTChecker] Support to mapping 2018-11-09 16:06:30 +00:00			`pragma experimental SMTChecker;`

			`contract C`
			`{`
			`mapping (bool => bool) map;`
			`function f(bool x) public view {`
			`require(x);`
			`assert(x != map[x]);`
			`}`
			`}`
Set tests that CVC4 can't handle to Z3 only 2019-12-04 15:39:34 +00:00			`// ====`
			`// SMTSolvers: z3`