// Testfile dumped by Ultimate at 2013/11/24 03:46:14

assert(!buchiIsEmpty(nwa));
assert(numberOfStates(removeNonLiveStates(nwa)) == 51);

NestedWordAutomaton nwa = (
    callAlphabet = {"c1" "c2" "c0" "c5" "c4" "c3" },
    internalAlphabet = {"a63" "a64" "a61" "a62" "a60" "a59" "a58" "a57" "a56" "a55" "a54" "a72" "a73" "a74" "a75" "a110" "a70" "a71" "a113" "a69" "a112" "a111" "a66" "a65" "a68" "a67" "a41" "a42" "a0" "a40" "a9" "a1" "a35" "a2" "a34" "a3" "a33" "a4" "a32" "a5" "a39" "a6" "a38" "a7" "a37" "a8" "a36" "a50" "a51" "a52" "a53" "a44" "a43" "a46" "a45" "a48" "a47" "a49" "a98" "a99" "a20" "a16" "a17" "a14" "a15" "a12" "a13" "a10" "a11" "a18" "a19" "a31" "a30" "a25" "a26" "a27" "a28" "a21" "a22" "a23" "a24" "a29" "a76" "a77" "a78" "a79" "a80" "a82" "a81" "a84" "a83" "a86" "a85" "a102" "a89" "a103" "a87" "a100" "a88" "a101" "a106" "a107" "a104" "a105" "a108" "a109" "a93" "a92" "a91" "a90" "a97" "a96" "a95" "a94" },
    returnAlphabet = {"r19" "r18" "r17" "r16" "r15" "r14" "r13" "r12" "r21" "r11" "r20" "r10" "r23" "r22" "r6" "r7" "r0" "r8" "r1" "r9" "r2" "r3" "r4" "r5" },
    states = {"s37" "s36" "s34" "s31" "s30" "s39" "s38" "s46" "s48" "s47" "s42" "s41" "s44" "s43" "s49" "s52" "s59" "s58" "s27" "s9" "s25" "s7" "s23" "s8" "s24" "s5" "s21" "s6" "s51" "s22" "s3" "s4" "s20" "s0" "s66" "s2" "s1" "s65" "s67" "s69" "s16" "s17" "s18" "s19" "s12" "s13" "s14" "s15" "s10" "s62" "s11" },
    initialStates = {"s6" },
    finalStates = {"s10" },
    callTransitions = {
         ("s2" "c2" "s1")
         ("s65" "c3" "s67")
         ("s14" "c5" "s12")
         ("s11" "c1" "s9")
         ("s62" "c3" "s66")
    },
    internalTransitions = {
         ("s37" "a43" "s23")
         ("s37" "a45" "s30")
         ("s36" "a0" "s30")
         ("s36" "a2" "s23")
         ("s34" "a93" "s36")
         ("s34" "a92" "s37")
         ("s31" "a9" "s25")
         ("s30" "a23" "s62")
         ("s30" "a24" "s11")
         ("s38" "a91" "s36")
         ("s38" "a94" "s24")
         ("s48" "a111" "s39")
         ("s48" "a48" "s42")
         ("s47" "a69" "s41")
         ("s47" "a65" "s52")
         ("s41" "a52" "s43")
         ("s41" "a47" "s39")
         ("s44" "a9" "s37")
         ("s44" "a11" "s36")
         ("s49" "a66" "s51")
         ("s52" "a50" "s42")
         ("s52" "a51" "s39")
         ("s59" "a82" "s15")
         ("s59" "a83" "s16")
         ("s58" "a89" "s49")
         ("s27" "a23" "s65")
         ("s25" "a45" "s27")
         ("s9" "a80" "s10")
         ("s9" "a81" "s8")
         ("s23" "a20" "s11")
         ("s23" "a19" "s62")
         ("s7" "a35" "s18")
         ("s7" "a34" "s22")
         ("s7" "a33" "s17")
         ("s24" "a41" "s13")
         ("s24" "a38" "s23")
         ("s8" "a16" "s22")
         ("s8" "a17" "s21")
         ("s8" "a15" "s19")
         ("s8" "a18" "s20")
         ("s5" "a6" "s4")
         ("s21" "a82" "s15")
         ("s21" "a83" "s16")
         ("s6" "a29" "s5")
         ("s51" "a48" "s46")
         ("s22" "a10" "s16")
         ("s3" "a58" "s2")
         ("s4" "a74" "s3")
         ("s20" "a87" "s16")
         ("s20" "a86" "s15")
         ("s0" "a41" "s13")
         ("s66" "a77" "s8")
         ("s66" "a75" "s10")
         ("s1" "a107" "s0")
         ("s67" "a77" "s69")
         ("s69" "a17" "s59")
         ("s69" "a15" "s58")
         ("s16" "a62" "s52")
         ("s16" "a66" "s48")
         ("s17" "a84" "s15")
         ("s17" "a85" "s47")
         ("s18" "a13" "s47")
         ("s18" "a90" "s15")
         ("s19" "a89" "s49")
         ("s12" "a78" "s10")
         ("s12" "a79" "s7")
         ("s13" "a21" "s14")
         ("s13" "a22" "s11")
         ("s15" "a70" "s52")
         ("s15" "a67" "s48")
         ("s10" "a31" "s22")
         ("s10" "a30" "s21")
         ("s10" "a32" "s19")
         ("s10" "a36" "s20")
    },
    returnTransitions = {
         ("s39" "s65" "r6" "s34")
         ("s39" "s62" "r6" "s34")
         ("s39" "s11" "r20" "s34")
         ("s39" "s14" "r22" "s34")
         ("s46" "s14" "r7" "s31")
         ("s46" "s65" "r9" "s31")
         ("s46" "s62" "r9" "s31")
         ("s46" "s11" "r5" "s31")
         ("s42" "s14" "r7" "s44")
         ("s42" "s65" "r9" "s44")
         ("s42" "s62" "r9" "s44")
         ("s42" "s11" "r5" "s44")
         ("s43" "s14" "r11" "s38")
    }
);