contract C {
}
// ====
// SMTEngine: all
// ----