CHECK( init(main()), LTL(G ! call(__VERIFIER_error())) )