// Testfile dumped by Ultimate at 2011/12/14 15:24:37

NestedWordAutomaton preprocessed = removeUnreachable(nwa);

int minimizeSevpaSize = numberOfStates(minimizeSevpa(preprocessed));
int shrinkNwaSize = numberOfStates(shrinkNwa(preprocessed));
int minimizeNwaPmaxSatDirectBiSize = numberOfStates(minimizeNwaPmaxSatDirectBi(preprocessed));
int minimizeNwaPmaxSatDirectSize = numberOfStates(minimizeNwaPmaxSatDirect(preprocessed));
int minimizeDfaSimulationSize = numberOfStates(minimizeDfaSimulation(preprocessed));
int reduceNwaDirectSimulationSize = numberOfStates(reduceNwaDirectSimulation(preprocessed));
int reduceNwaDirectSimulationBSize = numberOfStates(reduceNwaDirectSimulationB(preprocessed));
int reduceNwaDirectFullMultipebbleSimulationSize = numberOfStates(reduceNwaDirectFullMultipebbleSimulation(preprocessed));
int buchiReduceSize = numberOfStates(buchiReduce(preprocessed));
int reduceNwaDelayedSimulationSize = numberOfStates(reduceNwaDelayedSimulation(preprocessed));
int reduceNwaDelayedSimulationBSize = numberOfStates(reduceNwaDelayedSimulationB(preprocessed));
// int reduceNwaDelayedFullMultipebbleSimulationSize = numberOfStates(reduceNwaDelayedFullMultipebbleSimulation(preprocessed));
int reduceBuchiFairDirectSimulationSize = numberOfStates(reduceBuchiFairDirectSimulation(preprocessed));
int reduceBuchiFairSimulationSize = numberOfStates(reduceBuchiFairSimulation(preprocessed));

assert(minimizeSevpaSize == 8);
assert(shrinkNwaSize == 8);
assert(minimizeNwaPmaxSatDirectBiSize == 8);
assert(minimizeNwaPmaxSatDirectSize == 8);
assert(minimizeDfaSimulationSize == 8);
assert(reduceNwaDirectSimulationSize == 8);
assert(reduceNwaDirectSimulationBSize == 8);
assert(reduceNwaDirectFullMultipebbleSimulationSize == 8);
assert(buchiReduceSize == 8);
assert(reduceNwaDelayedSimulationSize == 8);
assert(reduceNwaDelayedSimulationBSize == 8);
// assert(reduceNwaDelayedFullMultipebbleSimulationSize == 8);
assert(reduceBuchiFairDirectSimulationSize == 8);
assert(reduceBuchiFairSimulationSize == 8);

NestedWordAutomaton nwa = (
	alphabet = {"[assume !(x2 == 0);, x2 = 0;]284" "[assume true;]237" "[assume !(x3 == 0);, x3 = 0;]130" "[assume x3 == 0;, x3 = 1;]25" "[assume x0 == 0;, x0 = 1;]41" "[assume x2 == 0;, x2 = 1;]280" "[assume !(x1 == 0);, x1 = 0;]50" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "[assume x3 == 0;]188" "[assume x1 == 0;, x1 = 1;]140" "[assume x3 != 0;]250" "[assume !(x0 == 0);, x0 = 0;]119" "[assume !(x3 == 0);]300" "[assume !(x3 != 0);]132" },
	states = {"{$emptyStack=false}_140" "{$emptyStack=false}_150" "{$emptyStack=false}_120" "{$emptyStack=(= v__x0 1)}_30" "{$emptyStack=false}_130" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90" "{$emptyStack=false}_110" "{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100" "{$emptyStack=false}_200" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80" "{$emptyStack=(not (= 0 1))}_40" "{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70" "{$emptyStack=(not (= 0 1))}_50" "{$emptyStack=true}_10" "{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60" "{$emptyStack=false}_180" "{$emptyStack=false}_190" "{$emptyStack=false}_160" "{$emptyStack=false}_170" },
	initialStates = {"{$emptyStack=true}_10" },
	finalStates = {"{$emptyStack=false}_140" "{$emptyStack=false}_150" "{$emptyStack=false}_120" "{$emptyStack=false}_130" "{$emptyStack=false}_110" "{$emptyStack=false}_200" "{$emptyStack=false}_180" "{$emptyStack=false}_190" "{$emptyStack=false}_160" "{$emptyStack=false}_170" },
	transitions = {
		("{$emptyStack=false}_140" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=false}_140")
		("{$emptyStack=false}_140" "[assume true;]237" "{$emptyStack=false}_120")
		("{$emptyStack=false}_140" "[assume !(x3 == 0);, x3 = 0;]130" "{$emptyStack=false}_110")
		("{$emptyStack=false}_140" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=false}_150")
		("{$emptyStack=false}_140" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=false}_110")
		("{$emptyStack=false}_140" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=false}_110")
		("{$emptyStack=false}_140" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=false}_140")
		("{$emptyStack=false}_140" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=false}_120")
		("{$emptyStack=false}_140" "[assume x3 == 0;]188" "{$emptyStack=false}_160")
		("{$emptyStack=false}_140" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=false}_110")
		("{$emptyStack=false}_140" "[assume x3 != 0;]250" "{$emptyStack=false}_120")
		("{$emptyStack=false}_140" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=false}_140")
		("{$emptyStack=false}_140" "[assume !(x3 == 0);]300" "{$emptyStack=false}_120")
		("{$emptyStack=false}_140" "[assume !(x3 != 0);]132" "{$emptyStack=false}_120")
		("{$emptyStack=false}_150" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=false}_190")
		("{$emptyStack=false}_150" "[assume true;]237" "{$emptyStack=false}_120")
		("{$emptyStack=false}_150" "[assume !(x3 == 0);, x3 = 0;]130" "{$emptyStack=false}_120")
		("{$emptyStack=false}_150" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=false}_150")
		("{$emptyStack=false}_150" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=false}_200")
		("{$emptyStack=false}_150" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=false}_180")
		("{$emptyStack=false}_150" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=false}_190")
		("{$emptyStack=false}_150" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=false}_130")
		("{$emptyStack=false}_150" "[assume x3 == 0;]188" "{$emptyStack=false}_160")
		("{$emptyStack=false}_150" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=false}_180")
		("{$emptyStack=false}_150" "[assume x3 != 0;]250" "{$emptyStack=false}_120")
		("{$emptyStack=false}_150" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=false}_190")
		("{$emptyStack=false}_150" "[assume !(x3 == 0);]300" "{$emptyStack=false}_120")
		("{$emptyStack=false}_150" "[assume !(x3 != 0);]132" "{$emptyStack=false}_120")
		("{$emptyStack=false}_120" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=false}_120")
		("{$emptyStack=false}_120" "[assume true;]237" "{$emptyStack=false}_120")
		("{$emptyStack=false}_120" "[assume !(x3 == 0);, x3 = 0;]130" "{$emptyStack=false}_120")
		("{$emptyStack=false}_120" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=false}_120")
		("{$emptyStack=false}_120" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=false}_120")
		("{$emptyStack=false}_120" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=false}_120")
		("{$emptyStack=false}_120" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=false}_120")
		("{$emptyStack=false}_120" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=false}_120")
		("{$emptyStack=false}_120" "[assume x3 == 0;]188" "{$emptyStack=false}_160")
		("{$emptyStack=false}_120" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=false}_120")
		("{$emptyStack=false}_120" "[assume x3 != 0;]250" "{$emptyStack=false}_120")
		("{$emptyStack=false}_120" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=false}_120")
		("{$emptyStack=false}_120" "[assume !(x3 == 0);]300" "{$emptyStack=false}_120")
		("{$emptyStack=false}_120" "[assume !(x3 != 0);]132" "{$emptyStack=false}_120")
		("{$emptyStack=(= v__x0 1)}_30" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=(= v__x0 1)}_30")
		("{$emptyStack=(= v__x0 1)}_30" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=true}_10")
		("{$emptyStack=(= v__x0 1)}_30" "[assume x3 == 0;]188" "{$emptyStack=(= v__x0 1)}_30")
		("{$emptyStack=(= v__x0 1)}_30" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=(not (= 0 1))}_40")
		("{$emptyStack=false}_130" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=false}_120")
		("{$emptyStack=false}_130" "[assume true;]237" "{$emptyStack=false}_120")
		("{$emptyStack=false}_130" "[assume !(x3 == 0);, x3 = 0;]130" "{$emptyStack=false}_120")
		("{$emptyStack=false}_130" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=false}_120")
		("{$emptyStack=false}_130" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=false}_170")
		("{$emptyStack=false}_130" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=false}_120")
		("{$emptyStack=false}_130" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=false}_120")
		("{$emptyStack=false}_130" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=false}_130")
		("{$emptyStack=false}_130" "[assume x3 == 0;]188" "{$emptyStack=false}_160")
		("{$emptyStack=false}_130" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=false}_120")
		("{$emptyStack=false}_130" "[assume x3 != 0;]250" "{$emptyStack=false}_120")
		("{$emptyStack=false}_130" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=false}_120")
		("{$emptyStack=false}_130" "[assume !(x3 == 0);]300" "{$emptyStack=false}_120")
		("{$emptyStack=false}_130" "[assume !(x3 != 0);]132" "{$emptyStack=false}_120")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90" "[assume !(x3 == 0);, x3 = 0;]130" "{$emptyStack=false}_110")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=true}_10")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90" "[assume x3 == 0;]188" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100")
		("{$emptyStack=false}_110" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=false}_140")
		("{$emptyStack=false}_110" "[assume true;]237" "{$emptyStack=false}_120")
		("{$emptyStack=false}_110" "[assume !(x3 == 0);, x3 = 0;]130" "{$emptyStack=false}_110")
		("{$emptyStack=false}_110" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=false}_150")
		("{$emptyStack=false}_110" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=false}_110")
		("{$emptyStack=false}_110" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=false}_110")
		("{$emptyStack=false}_110" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=false}_140")
		("{$emptyStack=false}_110" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=false}_130")
		("{$emptyStack=false}_110" "[assume x3 == 0;]188" "{$emptyStack=false}_160")
		("{$emptyStack=false}_110" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=false}_110")
		("{$emptyStack=false}_110" "[assume x3 != 0;]250" "{$emptyStack=false}_120")
		("{$emptyStack=false}_110" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=false}_140")
		("{$emptyStack=false}_110" "[assume !(x3 == 0);]300" "{$emptyStack=false}_120")
		("{$emptyStack=false}_110" "[assume !(x3 != 0);]132" "{$emptyStack=false}_120")
		("{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100")
		("{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100" "[assume !(x3 == 0);, x3 = 0;]130" "{$emptyStack=false}_110")
		("{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90")
		("{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60")
		("{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90")
		("{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100")
		("{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100" "[assume x3 == 0;]188" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80")
		("{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90")
		("{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100")
		("{$emptyStack=false}_200" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=false}_190")
		("{$emptyStack=false}_200" "[assume true;]237" "{$emptyStack=false}_120")
		("{$emptyStack=false}_200" "[assume !(x3 == 0);, x3 = 0;]130" "{$emptyStack=false}_120")
		("{$emptyStack=false}_200" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=false}_200")
		("{$emptyStack=false}_200" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=false}_150")
		("{$emptyStack=false}_200" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=false}_180")
		("{$emptyStack=false}_200" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=false}_190")
		("{$emptyStack=false}_200" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=false}_130")
		("{$emptyStack=false}_200" "[assume x3 == 0;]188" "{$emptyStack=false}_160")
		("{$emptyStack=false}_200" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=false}_180")
		("{$emptyStack=false}_200" "[assume x3 != 0;]250" "{$emptyStack=false}_120")
		("{$emptyStack=false}_200" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=false}_190")
		("{$emptyStack=false}_200" "[assume !(x3 == 0);]300" "{$emptyStack=false}_120")
		("{$emptyStack=false}_200" "[assume !(x3 != 0);]132" "{$emptyStack=false}_120")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80" "[assume !(x3 == 0);, x3 = 0;]130" "{$emptyStack=false}_110")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=true}_10")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80" "[assume x3 == 0;]188" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_90")
		("{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=(and (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_100")
		("{$emptyStack=(not (= 0 1))}_40" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=(not (= 0 1))}_40")
		("{$emptyStack=(not (= 0 1))}_40" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70")
		("{$emptyStack=(not (= 0 1))}_40" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60")
		("{$emptyStack=(not (= 0 1))}_40" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=(not (= 0 1))}_50")
		("{$emptyStack=(not (= 0 1))}_40" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=(not (= 0 1))}_40")
		("{$emptyStack=(not (= 0 1))}_40" "[assume x3 == 0;]188" "{$emptyStack=(not (= 0 1))}_50")
		("{$emptyStack=(not (= 0 1))}_40" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=(not (= 0 1))}_50")
		("{$emptyStack=(not (= 0 1))}_40" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=(not (= 0 1))}_40")
		("{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=(not (= 0 1))}_40")
		("{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70")
		("{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60")
		("{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=(not (= 0 1))}_50")
		("{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=(not (= 0 1))}_40")
		("{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=true}_10")
		("{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70" "[assume x3 == 0;]188" "{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70")
		("{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=(not (= 0 1))}_50")
		("{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=(not (= 0 1))}_40")
		("{$emptyStack=(not (= 0 1))}_50" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=(not (= 0 1))}_40")
		("{$emptyStack=(not (= 0 1))}_50" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70")
		("{$emptyStack=(not (= 0 1))}_50" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60")
		("{$emptyStack=(not (= 0 1))}_50" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=(not (= 0 1))}_50")
		("{$emptyStack=(not (= 0 1))}_50" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=(not (= 0 1))}_40")
		("{$emptyStack=(not (= 0 1))}_50" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=true}_10")
		("{$emptyStack=(not (= 0 1))}_50" "[assume x3 == 0;]188" "{$emptyStack=(not (= 0 1))}_50")
		("{$emptyStack=(not (= 0 1))}_50" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=(not (= 0 1))}_50")
		("{$emptyStack=(not (= 0 1))}_50" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=(not (= 0 1))}_40")
		("{$emptyStack=true}_10" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=(= v__x0 1)}_30")
		("{$emptyStack=true}_10" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=true}_10")
		("{$emptyStack=true}_10" "[assume x3 == 0;]188" "{$emptyStack=true}_10")
		("{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=(not (= 0 1))}_40")
		("{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=(and (not (= 0 1)) (= v__x0 1))}_70")
		("{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60")
		("{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=(not (= 0 1))}_50")
		("{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=(not (= 0 1))}_40")
		("{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=true}_10")
		("{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60" "[assume x3 == 0;]188" "{$emptyStack=(and (= v__x0 1) (= v__x3 0) (not (= 0 1)) (= v__x3 1))}_80")
		("{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=(not (= 0 1))}_50")
		("{$emptyStack=(and (not (= 0 1)) (= v__x3 1))}_60" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=(not (= 0 1))}_40")
		("{$emptyStack=false}_180" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=false}_190")
		("{$emptyStack=false}_180" "[assume true;]237" "{$emptyStack=false}_120")
		("{$emptyStack=false}_180" "[assume !(x3 == 0);, x3 = 0;]130" "{$emptyStack=false}_120")
		("{$emptyStack=false}_180" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=false}_150")
		("{$emptyStack=false}_180" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=false}_200")
		("{$emptyStack=false}_180" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=false}_180")
		("{$emptyStack=false}_180" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=false}_190")
		("{$emptyStack=false}_180" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=false}_130")
		("{$emptyStack=false}_180" "[assume x3 == 0;]188" "{$emptyStack=false}_160")
		("{$emptyStack=false}_180" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=false}_180")
		("{$emptyStack=false}_180" "[assume x3 != 0;]250" "{$emptyStack=false}_120")
		("{$emptyStack=false}_180" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=false}_190")
		("{$emptyStack=false}_180" "[assume !(x3 == 0);]300" "{$emptyStack=false}_120")
		("{$emptyStack=false}_180" "[assume !(x3 != 0);]132" "{$emptyStack=false}_120")
		("{$emptyStack=false}_190" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=false}_190")
		("{$emptyStack=false}_190" "[assume true;]237" "{$emptyStack=false}_120")
		("{$emptyStack=false}_190" "[assume !(x3 == 0);, x3 = 0;]130" "{$emptyStack=false}_120")
		("{$emptyStack=false}_190" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=false}_150")
		("{$emptyStack=false}_190" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=false}_200")
		("{$emptyStack=false}_190" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=false}_180")
		("{$emptyStack=false}_190" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=false}_190")
		("{$emptyStack=false}_190" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=false}_120")
		("{$emptyStack=false}_190" "[assume x3 == 0;]188" "{$emptyStack=false}_160")
		("{$emptyStack=false}_190" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=false}_180")
		("{$emptyStack=false}_190" "[assume x3 != 0;]250" "{$emptyStack=false}_120")
		("{$emptyStack=false}_190" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=false}_190")
		("{$emptyStack=false}_190" "[assume !(x3 == 0);]300" "{$emptyStack=false}_120")
		("{$emptyStack=false}_190" "[assume !(x3 != 0);]132" "{$emptyStack=false}_120")
		("{$emptyStack=false}_160" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=false}_140")
		("{$emptyStack=false}_160" "[assume true;]237" "{$emptyStack=false}_120")
		("{$emptyStack=false}_160" "[assume !(x3 == 0);, x3 = 0;]130" "{$emptyStack=false}_110")
		("{$emptyStack=false}_160" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=false}_150")
		("{$emptyStack=false}_160" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=false}_110")
		("{$emptyStack=false}_160" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=false}_110")
		("{$emptyStack=false}_160" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=false}_140")
		("{$emptyStack=false}_160" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=false}_130")
		("{$emptyStack=false}_160" "[assume x3 == 0;]188" "{$emptyStack=false}_160")
		("{$emptyStack=false}_160" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=false}_110")
		("{$emptyStack=false}_160" "[assume x3 != 0;]250" "{$emptyStack=false}_120")
		("{$emptyStack=false}_160" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=false}_140")
		("{$emptyStack=false}_160" "[assume !(x3 == 0);]300" "{$emptyStack=false}_120")
		("{$emptyStack=false}_160" "[assume !(x3 != 0);]132" "{$emptyStack=false}_120")
		("{$emptyStack=false}_170" "[assume !(x2 == 0);, x2 = 0;]284" "{$emptyStack=false}_120")
		("{$emptyStack=false}_170" "[assume true;]237" "{$emptyStack=false}_120")
		("{$emptyStack=false}_170" "[assume !(x3 == 0);, x3 = 0;]130" "{$emptyStack=false}_120")
		("{$emptyStack=false}_170" "[assume x3 == 0;, x3 = 1;]25" "{$emptyStack=false}_120")
		("{$emptyStack=false}_170" "[assume x0 == 0;, x0 = 1;]41" "{$emptyStack=false}_170")
		("{$emptyStack=false}_170" "[assume x2 == 0;, x2 = 1;]280" "{$emptyStack=false}_120")
		("{$emptyStack=false}_170" "[assume !(x1 == 0);, x1 = 0;]50" "{$emptyStack=false}_120")
		("{$emptyStack=false}_170" "[x0 = 0;, x1 = 0;, x2 = 0;, x3 = 0;]14" "{$emptyStack=false}_130")
		("{$emptyStack=false}_170" "[assume x3 == 0;]188" "{$emptyStack=false}_160")
		("{$emptyStack=false}_170" "[assume x1 == 0;, x1 = 1;]140" "{$emptyStack=false}_120")
		("{$emptyStack=false}_170" "[assume x3 != 0;]250" "{$emptyStack=false}_120")
		("{$emptyStack=false}_170" "[assume !(x0 == 0);, x0 = 0;]119" "{$emptyStack=false}_190")
		("{$emptyStack=false}_170" "[assume !(x3 == 0);]300" "{$emptyStack=false}_120")
		("{$emptyStack=false}_170" "[assume !(x3 != 0);]132" "{$emptyStack=false}_120")
	}
);