polymorphism_CVC4,1.5.oracle 569 Bytes