ArrayStoreException in simpleMP

[ywei]

command is:
tass verify -verbose simpleMPSpec.mmp -np 2

Exception in thread "main" java.lang.ArrayStoreException: [Ledu.udel.cis.vsl.minimp.state.IF.FrameIF;

at edu.udel.cis.vsl.minimp.state.impl.ModelEnvironment.push(ModelEnvironment.java:209)
at edu.udel.cis.vsl.minimp.verify.std.Environment.push(Environment.java:116)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.executeInvocation(Executor.java:174)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.initialize(Executor.java:457)
at edu.udel.cis.vsl.minimp.semantics.impl.Executor.initialize(Executor.java:463)
at edu.udel.cis.vsl.minimp.verify.std.StateManager.initialState(StateManager.java:49)
at edu.udel.cis.vsl.minimp.verify.Verification.verify(Verification.java:74)
at edu.udel.cis.vsl.minimp.Minimp.verify(Minimp.java:412)
at edu.udel.cis.vsl.minimp.Minimp.main(Minimp.java:506)

It seems in edu.udel.cis.vsl.minimp.state.impl.ModelEnvironment.java, line 209, the method is trying to store an array into the entry of another 2-D array. Is it legal to do that?

[Stephen Siegel]

Problem was I had an array of Frame[] and I tried to stick into it a FrameIF[]. Changed all arrays of Frame[] to arrays of FrameIF[].