contract C
{
uint x;
modifier m {
require(x > 0);
_;
}
function f() m public {
assert(x > 0);
x = x + 1;
// ====
// SMTEngine: all
// ----