1 2 3 4 5 6 7 8 9 10
pragma experimental SMTChecker; // Branch does not touch variable a contract C { function f(uint x) public pure { uint a = 3; if (x > 10) { } assert(a == 3); } }