EOF() from eigentechniques can be integrated to s2dverification