1 2 3 4 5 6 7 8 9
pragma experimental SMTChecker; contract C { function f(bool x) public pure { uint a; if(x) a = 1; assert(!x || a > 0); } }