pragma experimental SMTChecker;
contract C
{
mapping (bool => bool) map;
function f(bool x) public view {
require(x);
assert(x != map[x]);
}
// ====
// SMTSolvers: z3