id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
60	ArrayStoreException in simpleMP	ywei	Stephen Siegel	"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?"	defect	closed	major		state	1.0	fixed