// Testfile dumped by Ultimate at 2011/11/28 01:12:56

BranchingProcess bp = finitePrefix(net);
print(numberOfConditions(bp));
assert(numberOfConditions(bp) == 143);

assert(!isEmpty(net));

PetriNet net = (
	alphabet = {"[assume !(critical == 0);]262" "[assume !true;]31" "[n0 = 0;]186" "[critical = 0;]141" "[assume true;]38" "[assume true;]256" "[assume !true;]127" "[critical = 1;]255" "[assume true;]317" "[n1 = n0 + 1;]229" "[assume critical == 0;]43" "[critical = 0;]11" "[n1 = 0;]235" "[assume n0 == 0 || n1 < n0;]178" "[assume critical == 0;]277" "[critical = 1;]172" "[assume !(critical == 0);]315" "[n1 = 1;]323" "[critical = 0;]88" "[n0 = n1 + 1;]290" "[n0 = 0;]89" "[assume n1 == 0 || n0 < n1;]71" "[assume true;]130" "[assume true;]60" },
	places = {"#68##59#InitializeSharedVariablesINIT.20" "#69##60#InitializeSharedVariablesFINAL0" "#70#{$emptyStack=true}0" "#71#{$emptyStack=true}0" "#64##57#InitializeSharedVariablesINIT0" "#65##58#InitializeSharedVariablesINIT.10" "#66##55#$Ultimate##2.50" "#67##56#$Ultimate##2.70" "#72#{$emptyStack=(= v__critical 0)}0" "#73#{$emptyStack=(= v__critical 0)}0" "#42##33#$Ultimate##2.60" "#43##34#$Ultimate##2.50" "#46##38#$Ultimate##2.10" "#47##37#$Ultimate##2.70" "#44##36#Thread0EXIT0" "#45##35#Thread0FINAL0" "#51##41#$Ultimate##2.3Violation0" "#50##42#$Ultimate##2.40" "#49##39#$Ultimate##2.20" "#48##40#$Ultimate##2.30" "#55##45#InitializeSharedVariablesINIT.20" "#54##46#InitializeSharedVariablesFINAL0" "#53##43#InitializeSharedVariablesINIT0" "#52##44#InitializeSharedVariablesINIT.10" "#59##49#Thread1EXIT0" "#58##50#$Ultimate##2.30" "#57##47#Thread1FINAL0" "#56##48#$Ultimate##2.10" "#63##52#$Ultimate##2.40" "#62##51#$Ultimate##2.20" "#61##54#$Ultimate##2.60" "#60##53#$Ultimate##2.3Violation0" },
	transitions = {
		( {"#57##47#Thread1FINAL0" } "[assume true;]317" {"#59##49#Thread1EXIT0" } )
		( {"#47##37#$Ultimate##2.70" } "[assume true;]38" {"#46##38#$Ultimate##2.10" } )
		( {"#46##38#$Ultimate##2.10" } "[n0 = n1 + 1;]290" {"#49##39#$Ultimate##2.20" } )
		( {"#58##50#$Ultimate##2.30" "#73#{$emptyStack=(= v__critical 0)}0" } "[assume !(critical == 0);]262" {"#60##53#$Ultimate##2.3Violation0" "#73#{$emptyStack=(= v__critical 0)}0" } )
		( {"#66##55#$Ultimate##2.50" "#70#{$emptyStack=true}0" "#73#{$emptyStack=(= v__critical 0)}0" } "[critical = 0;]88" {"#61##54#$Ultimate##2.60" "#72#{$emptyStack=(= v__critical 0)}0" "#71#{$emptyStack=true}0" } )
		( {"#48##40#$Ultimate##2.30" "#71#{$emptyStack=true}0" } "[assume critical == 0;]43" {"#50##42#$Ultimate##2.40" "#71#{$emptyStack=true}0" } )
		( {"#48##40#$Ultimate##2.30" "#73#{$emptyStack=(= v__critical 0)}0" } "[assume !(critical == 0);]315" {"#51##41#$Ultimate##2.3Violation0" "#73#{$emptyStack=(= v__critical 0)}0" } )
		( {"#49##39#$Ultimate##2.20" } "[assume n1 == 0 || n0 < n1;]71" {"#48##40#$Ultimate##2.30" } )
		( {"#45##35#Thread0FINAL0" } "[assume true;]256" {"#44##36#Thread0EXIT0" } )
		( {"#58##50#$Ultimate##2.30" "#71#{$emptyStack=true}0" } "[assume critical == 0;]277" {"#63##52#$Ultimate##2.40" "#71#{$emptyStack=true}0" } )
		( {"#67##56#$Ultimate##2.70" "#73#{$emptyStack=(= v__critical 0)}0" "#71#{$emptyStack=true}0" } "[assume !true;]127" {"#57##47#Thread1FINAL0" "#73#{$emptyStack=(= v__critical 0)}0" "#71#{$emptyStack=true}0" } )
		( {"#63##52#$Ultimate##2.40" "#72#{$emptyStack=(= v__critical 0)}0" "#71#{$emptyStack=true}0" } "[critical = 1;]255" {"#66##55#$Ultimate##2.50" "#70#{$emptyStack=true}0" "#73#{$emptyStack=(= v__critical 0)}0" } )
		( {"#50##42#$Ultimate##2.40" "#72#{$emptyStack=(= v__critical 0)}0" "#71#{$emptyStack=true}0" } "[critical = 1;]172" {"#43##34#$Ultimate##2.50" "#70#{$emptyStack=true}0" "#73#{$emptyStack=(= v__critical 0)}0" } )
		( {"#53##43#InitializeSharedVariablesINIT0" "#64##57#InitializeSharedVariablesINIT0" "#71#{$emptyStack=true}0" } "[critical = 0;]141" {"#52##44#InitializeSharedVariablesINIT.10" "#65##58#InitializeSharedVariablesINIT.10" "#71#{$emptyStack=true}0" } )
		( {"#47##37#$Ultimate##2.70" "#73#{$emptyStack=(= v__critical 0)}0" "#71#{$emptyStack=true}0" } "[assume !true;]31" {"#45##35#Thread0FINAL0" "#73#{$emptyStack=(= v__critical 0)}0" "#71#{$emptyStack=true}0" } )
		( {"#58##50#$Ultimate##2.30" "#70#{$emptyStack=true}0" "#73#{$emptyStack=(= v__critical 0)}0" } "[assume critical == 0;]277" {"#63##52#$Ultimate##2.40" "#72#{$emptyStack=(= v__critical 0)}0" "#71#{$emptyStack=true}0" } )
		( {"#63##52#$Ultimate##2.40" "#73#{$emptyStack=(= v__critical 0)}0" } "[critical = 1;]255" {"#66##55#$Ultimate##2.50" "#73#{$emptyStack=(= v__critical 0)}0" } )
		( {"#54##46#InitializeSharedVariablesFINAL0" "#69##60#InitializeSharedVariablesFINAL0" } "[assume true;]60" {"#47##37#$Ultimate##2.70" "#67##56#$Ultimate##2.70" } )
		( {"#62##51#$Ultimate##2.20" } "[assume n0 == 0 || n1 < n0;]178" {"#58##50#$Ultimate##2.30" } )
		( {"#42##33#$Ultimate##2.60" } "[n0 = 0;]186" {"#47##37#$Ultimate##2.70" } )
		( {"#53##43#InitializeSharedVariablesINIT0" "#64##57#InitializeSharedVariablesINIT0" "#70#{$emptyStack=true}0" "#73#{$emptyStack=(= v__critical 0)}0" } "[critical = 0;]141" {"#52##44#InitializeSharedVariablesINIT.10" "#65##58#InitializeSharedVariablesINIT.10" "#72#{$emptyStack=(= v__critical 0)}0" "#71#{$emptyStack=true}0" } )
		( {"#61##54#$Ultimate##2.60" } "[n1 = 0;]235" {"#67##56#$Ultimate##2.70" } )
		( {"#66##55#$Ultimate##2.50" "#71#{$emptyStack=true}0" } "[critical = 0;]88" {"#61##54#$Ultimate##2.60" "#71#{$emptyStack=true}0" } )
		( {"#52##44#InitializeSharedVariablesINIT.10" "#65##58#InitializeSharedVariablesINIT.10" } "[n0 = 0;]89" {"#55##45#InitializeSharedVariablesINIT.20" "#68##59#InitializeSharedVariablesINIT.20" } )
		( {"#50##42#$Ultimate##2.40" "#73#{$emptyStack=(= v__critical 0)}0" } "[critical = 1;]172" {"#43##34#$Ultimate##2.50" "#73#{$emptyStack=(= v__critical 0)}0" } )
		( {"#43##34#$Ultimate##2.50" "#71#{$emptyStack=true}0" } "[critical = 0;]11" {"#42##33#$Ultimate##2.60" "#71#{$emptyStack=true}0" } )
		( {"#67##56#$Ultimate##2.70" } "[assume true;]130" {"#56##48#$Ultimate##2.10" } )
		( {"#55##45#InitializeSharedVariablesINIT.20" "#68##59#InitializeSharedVariablesINIT.20" } "[n1 = 1;]323" {"#54##46#InitializeSharedVariablesFINAL0" "#69##60#InitializeSharedVariablesFINAL0" } )
		( {"#43##34#$Ultimate##2.50" "#70#{$emptyStack=true}0" "#73#{$emptyStack=(= v__critical 0)}0" } "[critical = 0;]11" {"#42##33#$Ultimate##2.60" "#72#{$emptyStack=(= v__critical 0)}0" "#71#{$emptyStack=true}0" } )
		( {"#56##48#$Ultimate##2.10" } "[n1 = n0 + 1;]229" {"#62##51#$Ultimate##2.20" } )
		( {"#48##40#$Ultimate##2.30" "#70#{$emptyStack=true}0" "#73#{$emptyStack=(= v__critical 0)}0" } "[assume critical == 0;]43" {"#50##42#$Ultimate##2.40" "#72#{$emptyStack=(= v__critical 0)}0" "#71#{$emptyStack=true}0" } )
	},
	initialMarking = {"#70#{$emptyStack=true}0" "#64##57#InitializeSharedVariablesINIT0" "#53##43#InitializeSharedVariablesINIT0" "#73#{$emptyStack=(= v__critical 0)}0" },
	acceptingPlaces = {"#51##41#$Ultimate##2.3Violation0" "#60##53#$Ultimate##2.3Violation0" }
);