int main(){
  __VERIFIER_assume(0);
}