// Testfile dumped by Ultimate at 2020/04/24 15:58:03
//
// 

assert(!isEmpty(nwa));
assert(!isEmptyHeuristic(nwa));


NestedWordAutomaton nwa = (
	callAlphabet = {c0 c1 c2 c3 },
	internalAlphabet = {a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 a10 a11 a12 },
	returnAlphabet = {r0 r1 r2 r3 },
	states = {s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 },
	initialStates = {s3 },
	finalStates = {s6 },
	callTransitions = {
		(s1 c3 s13)
		(s3 c1 s5)
		(s8 c0 s9)
		(s9 c2 s10)
		(s12 c3 s13)
	},
	internalTransitions = {
		(s0 a8 s2)
		(s4 a5 s6)
		(s5 a7 s7)
		(s10 a12 s11)
		(s11 a4 s12)
		(s13 a12 s14)
		(s14 a11 s0)
		(s14 a4 s1)
	},
	returnTransitions = {
		(s2 s1 r0 s4)
		(s7 s3 r1 s8)
	}
);