pragma experimental SMTChecker;

contract C {
}