// Testfile dumped by Ultimate at 2015/10/05 04:05:45
//
// RefinementSetting [m_InterpolantAutomaton=ScroogeNondeterminism, m_BouncerStem=true, m_BouncerLoop=true, m_ScroogeNondeterminismStem=true, m_ScroogeNondeterminismLoop=false, m_CannibalizeLoop=false, m_UsedDefinedMaxRank=-3]

NestedWordAutomaton cNCSB = buchiComplementNCSB(nwa);
print(numberOfStates(cNCSB));

NestedWordAutomaton nwa = (
	callAlphabet = {},
	internalAlphabet = {"assume !!(main_~x~2 > 0 && main_~y~2 > 0);main_~old_x~3 := main_~x~2;main_~old_y~3 := main_~y~2;" "assume true;" "assume true;" "assume !(main_#t~nondet2 != 0);havoc main_#t~nondet2;main_~x~2 := main_~old_y~3 - 2;main_~y~2 := main_~old_x~3 + 1;" "havoc main_#res;havoc main_#t~nondet0, main_#t~nondet1, main_#t~nondet2, main_~old_x~3, main_~old_y~3, main_~x~2, main_~y~2;main_~x~2 := main_#t~nondet0;havoc main_#t~nondet0;main_~y~2 := main_#t~nondet1;havoc main_#t~nondet1;" "assume !(main_~x~2 > 0 && main_~y~2 > 0);" "assume main_#t~nondet2 != 0;havoc main_#t~nondet2;main_~x~2 := main_~old_x~3 - 1;main_~y~2 := main_~old_x~3;" "assume !true;" "main_#res := 0;#t~ret3 := main_#res;assume true;" },
	returnAlphabet = {},
	states = {"866588#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "875352#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0))" "830553#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))" "1174990#(and (<= 7 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "927571#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "1019768#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "844727#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "993862#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "828375#unseeded" "831894#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0))" "844694#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0))" "840086#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "927576#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "828719#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))" "875371#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "828716#(<= ULTIMATE.start_main_~old_x~3 oldRank0)" "828563#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))" "831913#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "828386#(<= ULTIMATE.start_main_~x~2 oldRank0)" "914710#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "828385#(and (<= 0 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0))" },
	initialStates = {"828375#unseeded" },
	finalStates = {"828385#(and (<= 0 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0))" },
	callTransitions = {
	},
	internalTransitions = {
		 ("866588#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "assume !(main_#t~nondet2 != 0);havoc main_#t~nondet2;main_~x~2 := main_~old_y~3 - 2;main_~y~2 := main_~old_x~3 + 1;" "875352#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0))")
		 ("866588#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "assume main_#t~nondet2 != 0;havoc main_#t~nondet2;main_~x~2 := main_~old_x~3 - 1;main_~y~2 := main_~old_x~3;" "875371#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))")
		 ("875352#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0))" "assume true;" "875352#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0))")
		 ("875352#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0))" "assume true;" "875352#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0))")
		 ("830553#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))" "assume !(main_#t~nondet2 != 0);havoc main_#t~nondet2;main_~x~2 := main_~old_y~3 - 2;main_~y~2 := main_~old_x~3 + 1;" "831894#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0))")
		 ("830553#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))" "assume main_#t~nondet2 != 0;havoc main_#t~nondet2;main_~x~2 := main_~old_x~3 - 1;main_~y~2 := main_~old_x~3;" "831913#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))")
		 ("1174990#(and (<= 7 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume true;" "828385#(and (<= 0 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0))")
		 ("1174990#(and (<= 7 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume !(main_#t~nondet2 != 0);havoc main_#t~nondet2;main_~x~2 := main_~old_y~3 - 2;main_~y~2 := main_~old_x~3 + 1;" "1174990#(and (<= 7 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("1174990#(and (<= 7 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume main_#t~nondet2 != 0;havoc main_#t~nondet2;main_~x~2 := main_~old_x~3 - 1;main_~y~2 := main_~old_x~3;" "1174990#(and (<= 7 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("927571#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume !!(main_~x~2 > 0 && main_~y~2 > 0);main_~old_x~3 := main_~x~2;main_~old_y~3 := main_~y~2;" "993862#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("927571#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume true;" "927571#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("927571#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume true;" "927571#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("1019768#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume !!(main_~x~2 > 0 && main_~y~2 > 0);main_~old_x~3 := main_~x~2;main_~old_y~3 := main_~y~2;" "1174990#(and (<= 7 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("1019768#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume true;" "1019768#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("1019768#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume true;" "1019768#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("844727#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "assume !!(main_~x~2 > 0 && main_~y~2 > 0);main_~old_x~3 := main_~x~2;main_~old_y~3 := main_~y~2;" "866588#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))")
		 ("844727#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "assume true;" "844727#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))")
		 ("844727#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "assume true;" "844727#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))")
		 ("993862#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume !(main_#t~nondet2 != 0);havoc main_#t~nondet2;main_~x~2 := main_~old_y~3 - 2;main_~y~2 := main_~old_x~3 + 1;" "1019768#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("993862#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume main_#t~nondet2 != 0;havoc main_#t~nondet2;main_~x~2 := main_~old_x~3 - 1;main_~y~2 := main_~old_x~3;" "1019768#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_y~3 4) oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 5) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 6) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("828375#unseeded" "assume !!(main_~x~2 > 0 && main_~y~2 > 0);main_~old_x~3 := main_~x~2;main_~old_y~3 := main_~y~2;" "828375#unseeded")
		 ("828375#unseeded" "assume true;" "828375#unseeded")
		 ("828375#unseeded" "assume true;" "828375#unseeded")
		 ("828375#unseeded" "assume true;" "828385#(and (<= 0 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0))")
		 ("828375#unseeded" "assume !(main_#t~nondet2 != 0);havoc main_#t~nondet2;main_~x~2 := main_~old_y~3 - 2;main_~y~2 := main_~old_x~3 + 1;" "828375#unseeded")
		 ("828375#unseeded" "havoc main_#res;havoc main_#t~nondet0, main_#t~nondet1, main_#t~nondet2, main_~old_x~3, main_~old_y~3, main_~x~2, main_~y~2;main_~x~2 := main_#t~nondet0;havoc main_#t~nondet0;main_~y~2 := main_#t~nondet1;havoc main_#t~nondet1;" "828375#unseeded")
		 ("828375#unseeded" "assume main_#t~nondet2 != 0;havoc main_#t~nondet2;main_~x~2 := main_~old_x~3 - 1;main_~y~2 := main_~old_x~3;" "828375#unseeded")
		 ("831894#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0))" "assume true;" "831894#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0))")
		 ("831894#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0))" "assume true;" "831894#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0))")
		 ("844694#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0))" "assume true;" "844694#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0))")
		 ("844694#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0))" "assume true;" "844694#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0))")
		 ("840086#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "assume !(main_#t~nondet2 != 0);havoc main_#t~nondet2;main_~x~2 := main_~old_y~3 - 2;main_~y~2 := main_~old_x~3 + 1;" "844694#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0))")
		 ("840086#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "assume main_#t~nondet2 != 0;havoc main_#t~nondet2;main_~x~2 := main_~old_x~3 - 1;main_~y~2 := main_~old_x~3;" "844727#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))")
		 ("927576#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume true;" "927576#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("927576#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume true;" "927576#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("828719#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))" "assume !!(main_~x~2 > 0 && main_~y~2 > 0);main_~old_x~3 := main_~x~2;main_~old_y~3 := main_~y~2;" "830553#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))")
		 ("828719#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))" "assume true;" "828719#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))")
		 ("828719#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))" "assume true;" "828719#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))")
		 ("875371#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "assume !!(main_~x~2 > 0 && main_~y~2 > 0);main_~old_x~3 := main_~x~2;main_~old_y~3 := main_~y~2;" "914710#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("875371#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "assume true;" "875371#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))")
		 ("875371#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "assume true;" "875371#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))")
		 ("828716#(<= ULTIMATE.start_main_~old_x~3 oldRank0)" "assume true;" "828716#(<= ULTIMATE.start_main_~old_x~3 oldRank0)")
		 ("828716#(<= ULTIMATE.start_main_~old_x~3 oldRank0)" "assume true;" "828716#(<= ULTIMATE.start_main_~old_x~3 oldRank0)")
		 ("828563#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))" "assume !(main_#t~nondet2 != 0);havoc main_#t~nondet2;main_~x~2 := main_~old_y~3 - 2;main_~y~2 := main_~old_x~3 + 1;" "828716#(<= ULTIMATE.start_main_~old_x~3 oldRank0)")
		 ("828563#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))" "assume main_#t~nondet2 != 0;havoc main_#t~nondet2;main_~x~2 := main_~old_x~3 - 1;main_~y~2 := main_~old_x~3;" "828719#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))")
		 ("831913#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "assume !!(main_~x~2 > 0 && main_~y~2 > 0);main_~old_x~3 := main_~x~2;main_~old_y~3 := main_~y~2;" "840086#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))")
		 ("831913#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "assume true;" "831913#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))")
		 ("831913#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))" "assume true;" "831913#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0))")
		 ("828386#(<= ULTIMATE.start_main_~x~2 oldRank0)" "assume !!(main_~x~2 > 0 && main_~y~2 > 0);main_~old_x~3 := main_~x~2;main_~old_y~3 := main_~y~2;" "828563#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0))")
		 ("914710#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume !(main_#t~nondet2 != 0);havoc main_#t~nondet2;main_~x~2 := main_~old_y~3 - 2;main_~y~2 := main_~old_x~3 + 1;" "927576#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("914710#(and (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))" "assume main_#t~nondet2 != 0;havoc main_#t~nondet2;main_~x~2 := main_~old_x~3 - 1;main_~y~2 := main_~old_x~3;" "927571#(and (<= (+ ULTIMATE.start_main_~x~2 5) oldRank0) (<= ULTIMATE.start_main_~old_x~3 oldRank0) (<= (+ ULTIMATE.start_main_~y~2 4) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 3) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 1) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 2) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 3) oldRank0) (<= (+ ULTIMATE.start_main_~x~2 4) oldRank0) (<= ULTIMATE.start_main_~x~2 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 2) oldRank0) (<= (+ ULTIMATE.start_main_~old_x~3 4) oldRank0))")
		 ("828385#(and (<= 0 oldRank0) (<= (+ ULTIMATE.start_main_~x~2 1) oldRank0))" "assume true;" "828386#(<= ULTIMATE.start_main_~x~2 oldRank0)")
	},
	returnTransitions = {
	}
);