id	summary	reporter	owner	description	type	status	priority	milestone	component	version	resolution	keywords	cc
268	no extra locations for collective assertions...	Stephen Siegel	zirkel	"A {joint,collective,} {assertion,invariant} specified as a pragma should never add a location to a model.  It should only set values in a particular location.   The philosophy is that you don't want ""Heisenbugs"" arising from modifying the model you are trying to analyze.

If the pragma is inserted in a ""bad"" place---a place that does not really have a location associated to it --- a syntax error should be thrown saying something to the effect ""No location at this position"".  The bad places are ends of blocks in ""if"" statements, loops, etc.

If a user wants to add a pragma at such a point, he can introduce a location by just adding a "";"" (empty statement) after the pragma.
"	defect	closed	major	1.1	front	1.1	fixed	pragma collective assertion invariant joint