Recursive python pickle files
### Depth 1 (pickled.py):
```python__import__('pickle').loads(b'(I128...')```
At this layer we get a long string loading a long string. Whenever pickle loads it, it starts to execute code. Python comes with a pickle disassembler, so let's try using that.
#### 1. Write to file
```pythont = b'(I128...)'f = open("pickled_l2.dat", "wb")f.write(t)f.close()```
#### 2. Call pickletools
```python -m pickletools pickled_l2.dat > pickled_l2.pkl```
The `stack not empty after STOP` is normal.
### Depth 2 (pickled_l2.pkl):
```asm     0: (    MARK     1: I        INT        128     6: I        INT        4...544265: I        INT        82544269: I        INT        46544273: t        TUPLE      (MARK at 0)544274: p    PUT        69420544281: c    GLOBAL     'pickle loads'544295: c    GLOBAL     'builtins bytes'544311: g    GET        69420544318: \x85 TUPLE1544319: R    REDUCE544320: \x85 TUPLE1544321: R    REDUCE544322: .    STOP```
'pickle loads' looks like it's loading another pickle file, so let's extract that into another file. I found it easiest to go into the original pickled_l2.dat file and replace all `I` with nothing, all newlines with `,`, then throw it into a python script and write out the contents.
#### 1. Write to file
```pythona=[128,4,99,112,105,99,107,108,...,82,46]f = open("pickled_l3.dat","wb")f.write(bytearray(a))f.close()```
#### 2. Call pickletools
```python -m pickletools pickled_l3.dat > pickled_l3.pkl```
### Depth 3 (pickled_l3.pkl):
The first half of the file has some constants and functions in pickle. You could decode them with pickletools, but it's pretty obvious what they're doing:
```pythondef pickledhorseradish(): return pickledmacadamia.__add__(pickledbarberry)def pickledcoconut(): return pickledmacadamia.__sub__(pickledbarberry)def pickledlychee(): return pickledmacadamia.__xor__(pickledbarberry)def pickledcrabapple(): return pickledmacadamia.__eq__(pickledbarberry)def pickledportabella(): return pickledmacadamia.__ne__(pickledbarberry)def pickledquince(): return pickledmacadamia.__le__(pickledbarberry)def pickledeasternmayhawthorn(): return pickledmacadamia.__ge__(pickledbarberry)def pickledmonstera(): return 1def pickledcorneliancherry(): return 0def pickledalligatorapple(): #???def pickledboysenberry(): #very long function```
Before we move onto the boysenberry function, we can also find that the input string is `pickledximenia` and its length should be 64:
```119509: \x86     TUPLE2119510: \x8c     SHORT_BINUNICODE 'pickledximenia'119526: c        GLOBAL     'builtins input'119542: \x8c     SHORT_BINUNICODE 'What is the flag? '119562: \x85     TUPLE1119563: R        REDUCE...119626: (    MARK119627: \x8c     SHORT_BINUNICODE 'pickledburmesegrape'119648: c        GLOBAL     'io pickledximenia.__len__'119675: )        EMPTY_TUPLE119676: R        REDUCE...119784: \x8c SHORT_BINUNICODE 'io'119788: c    GLOBAL     'io pickledgarlic.__getitem__'119818: c    GLOBAL     'io pickledburmesegrape.__eq__'119849: I    INT        64119853: \x85 TUPLE1119854: R    REDUCE```
#### 1. Write to file
```pythona=b'\x80\x04cpickle\nio\n(...dcedarbaycherry\n\x85R.'f = open("pickled_l4.dat","wb")f.write(a)f.close()```
#### 2. Call pickletools
```python -m pickletools pickled_l4.dat > pickled_l4.pkl```
### Depth 4 (pickled_l4.pkl):
There's a lot more pickle "programs" here, but really the one that has the start of the fun is in `pickledvoavanga`. It doesn't have a header, which is added from `pickledalligatorapple`. Instead of trying to understand what it was doing, I just called the original script, gave it a 64 length string, and printed the value.
```python>>> exec(open("chall.py").read())What is the flag? aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaNope!>>> import io>>> io.pickledalligatorappleb'\x80\x04I97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\nI97\n'```
So it seems to pass in our string as INT values. We can dump these values and then take a look at the first function, `pickledvoavanga` (with `pickledalligatorapple` prepended).
### Depth 5 (pickledvoavanga.pkl)
At the start, we see the ints from `pickledalligatorapple`, but also some pops/puts. This looks like the function is selecting which of the characters to use from the input.
```    0: \x80 PROTO      4    2: I    INT        97    6: I    INT        97...  246: I    INT        97  250: I    INT        97  254: I    INT        97  258: 0    POP  259: 0    POP...  265: 0    POP  266: 0    POP  267: p    PUT        1  270: 0    POP  271: 0    POP...  318: 0    POP  319: 0    POP  320: p    PUT        0  323: 0    POP  324: 0    POP  325: 0    POP  326: 0    POP  327: 0    POP```
Then there's the other logic
```  328: c    GLOBAL     'pickle io'  339: (    MARK  340: \x8c     SHORT_BINUNICODE 'pickledmacadamia'  358: g        GET        0  361: \x8c     SHORT_BINUNICODE 'pickledbarberry'  378: g        GET        1  381: \x8c     SHORT_BINUNICODE 'pickledgarlic'  396: \x8c     SHORT_BINUNICODE 'pickledcorneliancherry'  420: \x8c     SHORT_BINUNICODE 'pickledarugula'  436: \x86     TUPLE2  437: d        DICT       (MARK at 339)  438: b    BUILD  439: c    GLOBAL     'pickle loads'  453: \x8c SHORT_BINUNICODE 'io'  457: c    GLOBAL     'io pickledgarlic.__getitem__'  487: c    GLOBAL     'pickle loads'  501: c    GLOBAL     'io pickledeasternmayhawthorn'  531: \x85 TUPLE1  532: R    REDUCE```
Looks like a lot of these names are from the functions from `pickled_l3.pkl`. Let's try to decode some of these names to better understand what's going on.
```pickledmacadamia - left argumentpickledbarberry - right argumentpickledgarlic - tuple of these two values:  pickledcorneliancherry - return 0  pickledarugula - next function in pickled_l4.pklpickledeasternmayhawthorn - pickledmacadamia >= pickledbarberry```
So it looks like one character of the string is compared with another, and if it's valid, it continues on to the next function. We can write a script to read these functions, but there are actually two types of functions. Let's take a look at `pickledleeks`, the fourth function called.
```  327: 0    POP  328: c    GLOBAL     'pickle io'  339: (    MARK  340: \x8c     SHORT_BINUNICODE 'pickledmacadamia'  358: g        GET        0  361: \x8c     SHORT_BINUNICODE 'pickledbarberry'  378: g        GET        1  381: \x8c     SHORT_BINUNICODE 'pickledgarlic'  396: \x8c     SHORT_BINUNICODE 'pickledcorneliancherry'  420: \x8c     SHORT_BINUNICODE 'pickledjocote'  435: \x86     TUPLE2  436: d        DICT       (MARK at 339)  437: b    BUILD  438: c    GLOBAL     'pickle loads'  452: \x8c SHORT_BINUNICODE 'io'  456: c    GLOBAL     'io pickledgarlic.__getitem__'  486: c    GLOBAL     'pickle io'  497: (    MARK  498: \x8c     SHORT_BINUNICODE 'pickledmacadamia'  516: c        GLOBAL     'pickle loads'  530: c        GLOBAL     'io pickledlychee'  548: \x85     TUPLE1  549: R        REDUCE  550: \x8c     SHORT_BINUNICODE 'pickledbarberry'  567: I        INT        0  570: d        DICT       (MARK at 497)  571: b    BUILD  572: 0    POP  573: c    GLOBAL     'pickle loads'  587: c    GLOBAL     'io pickledcrabapple'  608: \x85 TUPLE1```
This one xors the first value with the second value, then compares it with the constant (0 on line 567). So we have to account for two types of checks being made.
#### 1. Dump all pickle functions script
Recursively dumps pickle "functions" starting at `pickled_l3.pkl`.
```pythonimport subprocessdef it(s):    tmpName = f"{s}.dat"    asmName = f"{s}.pkl"    subprocess.run(["python", "-m", "pickletools", tmpName, "-o", asmName])    f = open(asmName, "r")    lines = f.readlines()    content = [x.rstrip("\n") for x in lines]    name = "idkwhatthelastnamewas"    lastLine = ""    #print(f"opening {asmName}")    for line in lines:        if "SHORT_BINUNICODE" in line:            name = line.split("SHORT_BINUNICODE '", 1)[1][:-2]        elif "SHORT_BINBYTES" in line or "BINBYTES" in line:            dataName = f"__tmp_{name}.dat"            df = open(dataName, "wb")            s = line.split(" b'", 1)[1][:-2]            if "pickledalligatorapple" in lastLine:                s = "\\x80\\x04I97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\nI97\\n" + s            df.write(eval("b'" + s + "'"))            df.close()            it(name)        lastLine = line
it("pickled_l3")```
#### 2. Parse all pickle functions and export to z3 script
This script does some wacky hacky text file parsing to generate conditions. Simple to do by hand, but I just felt like making a script. Expects the pickle "functions" from `pickled_l4.pkl` to be disassembled to `{functionname}.pkl`
```python#quality code obv
def it(s):    asmName = f"{s}.pkl"    f = open(asmName, "r")    lines = f.readlines()    content = [x.rstrip("\n") for x in lines]    name = "idkwhatthelastnamewas"    lastLine = ""     pushing = True    popping = False    coding = False     fakeStack = []    var0 = 0    var1 = 0     mode = 0     #0 - entered first mark    #1 - exited first mark    #2 - entered second mark    #3 - exited second mark    mark = -1     poppedValue = -1     curCompName = "idkCompName"    curOpName = "idkOpName"     nextFunName = "dunnoNextFunName"     for line in lines:        if pushing:            if "\\x80 PROTO" in line:                pass            elif "I    INT" in line:                fakeStack.append(len(fakeStack))            else:                pushing = False                popping = True        if popping:            if "POP" in line:                poppedValue = fakeStack.pop()            elif "PUT        0" in line:                var0 = fakeStack[-1] #poppedValue            elif "PUT        1" in line:                var1 = fakeStack[-1]            else:                popping = False                coding = True        if "SHORT_BINUNICODE" in line:            if "pickledmacadamia" in line:                pass            elif "pickledbarberry" in line:                pass            elif "pickledgarlic" in line:                pass            elif "pickledcorneliancherry" in line:                pass            else:                if mode == 0:                    nextFunName = line.split("SHORT_BINUNICODE '", 1)[1][:-2]                    mode = 1        elif "(    MARK" in line:            mark += 1        elif "b    BUILD" in line:            mark += 1        elif mark == 2 and "c        GLOBAL" in line:            if "GLOBAL     'pickle loads'" in line:                pass            else:                curOpName = line.split("GLOBAL     'io ", 1)[1][:-2]        elif mark == 2 and "I        INT" in line:            curOpValue = line.split("INT        ", 1)[1][:-1]        elif (mark == 1 or mark == 3) and "c    GLOBAL" in line:            if "GLOBAL     'io pickledgarlic.__getitem__'" in line:                pass            elif "GLOBAL     'pickle loads'" in line:                pass            elif "GLOBAL     'pickle io'" in line:                pass            else:                curCompName = line.split("GLOBAL     'io ", 1)[1][:-2]     if curOpName == "pickledhorseradish":        curOpName = "+"    elif curOpName == "pickledcoconut":        curOpName = "-"    elif curOpName == "pickledlychee":        curOpName = "^"     if curCompName == "pickledcrabapple":        curCompName = "=="    elif curCompName == "pickledportabella":        curCompName = "!="    elif curCompName == "pickledquince":        curCompName = "<="    elif curCompName == "pickledeasternmayhawthorn":        curCompName = ">="     if mark == 3: #has operation        print(f"s.add((arr[{var0}] {curOpName} arr[{var1}]) {curCompName} {curOpValue}) # {s}")    else:        print(f"s.add(arr[{var0}] {curCompName} arr[{var1}]) # {s}")     it(nextFunName) it("pickledvoavanga")```
#### 3. Z3 script
```pythonfrom z3 import *
arr = [BitVec(f'{i}', 32) for i in range(64)]s = Solver()
for i in range(64):	s.add(arr[i] >= 32)	s.add(arr[i] <= 127)
s.add(arr[4] >= arr[54]) # pickledvoavangas.add(arr[6] <= arr[14]) # pickledarugulas.add(arr[36] >= arr[30]) # pickledhuckleberrys.add((arr[28] ^ arr[34]) == 0) # pickledleekss.add((arr[23] + arr[7]) == 218) # pickledjocotes.add((arr[55] ^ arr[31]) == 4) # pickledsugarapples.add(arr[58] != arr[18]) # pickledcollardgreenss.add((arr[40] + arr[56]) == 207) # pickledpassionfruits.add((arr[29] - arr[51]) == 59) # pickledplums.add((arr[12] ^ arr[60]) == 71) # pickledeightballsquashs.add(arr[48] <= arr[42]) # pickledchivess.add((arr[19] + arr[16]) == 198) # pickledalfalfasproutss.add(arr[59] != arr[49]) # pickledneems.add((arr[61] - arr[43]) == 13) # pickledmelons.add(arr[21] != arr[46]) # pickledcherrys.add(arr[39] != arr[13]) # pickledoranges.add((arr[9] - arr[38]) == 65) # pickledfibroussatinashs.add((arr[3] - arr[8]) == 8) # pickledorangelos.add((arr[17] - arr[26]) == 47) # pickledmountainsoursops.add((arr[45] - arr[20]) == 21) # pickledwildoranges.add(arr[5] >= arr[37]) # pickledsycamorefigs.add((arr[41] - arr[44]) == 68) # pickledthimbleberrys.add((arr[47] + arr[24]) == 217) # pickledvineripetomatoess.add((arr[10] + arr[2]) == 201) # pickledbambooshootss.add((arr[25] ^ arr[22]) == 93) # pickledkidneybeanss.add(arr[62] >= arr[52]) # pickledsweetlemons.add(arr[11] != arr[53]) # pickledjalapenos.add((arr[63] - arr[35]) == 26) # pickledpomcites.add((arr[33] - arr[50]) == 12) # pickledotaheiteapples.add(arr[15] != arr[0]) # pickledyumberrys.add((arr[32] ^ arr[1]) == 51) # pickledsnowpeass.add(arr[57] != arr[27]) # pickledfennels.add((arr[2] ^ arr[34]) == 80) # pickledlangsats.add((arr[27] - arr[53]) == 0) # pickledcamucamus.add((arr[7] + arr[52]) == 219) # pickledcempedaks.add(arr[23] <= arr[5]) # pickledjatobas.add(arr[49] <= arr[8]) # pickledmangosteens.add(arr[6] != arr[22]) # pickledgalias.add((arr[45] + arr[0]) == 218) # pickledemuapples.add(arr[30] == arr[14]) # pickledpeass.add((arr[63] + arr[10]) == 229) # pickledmandarins.add(arr[42] >= arr[19]) # pickledcabbages.add((arr[13] + arr[43]) == 148) # pickledpommecytheres.add(arr[57] != arr[17]) # pickledkohlrabis.add((arr[24] - arr[44]) == 58) # pickledpodocarpuss.add(arr[47] != arr[40]) # pickledsoursops.add(arr[9] >= arr[60]) # pickledkeppelfruits.add((arr[62] ^ arr[32]) == 47) # pickledackees.add((arr[20] + arr[21]) == 207) # pickledfijilongans.add(arr[28] <= arr[38]) # pickledgourdss.add(arr[29] >= arr[11]) # pickledmarangs.add((arr[46] + arr[26]) == 146) # pickledceylongooseberrys.add((arr[4] + arr[15]) == 175) # pickledrimus.add((arr[31] ^ arr[48]) == 7) # pickledbearberrys.add(arr[33] >= arr[18]) # pickleddavidsonsplums.add((arr[55] + arr[39]) == 143) # pickledillawarraplums.add(arr[36] != arr[58]) # pickledkandisfruits.add((arr[61] - arr[1]) == 0) # pickledkales.add(arr[50] != arr[41]) # pickledsnowberrys.add((arr[37] + arr[12]) == 224) # pickledkiwis.add(arr[3] != arr[59]) # pickleduvagrapes.add((arr[25] ^ arr[16]) == 51) # pickledlemons.add(arr[51] != arr[35]) # pickledarazas.add(arr[56] != arr[54]) # picklednativecherrys.add((arr[23] ^ arr[61]) == 15) # pickledmaypops.add((arr[52] - arr[31]) == 48) # pickledpulasans.add((arr[37] + arr[36]) == 215) # pickledhawthorns.add((arr[57] - arr[60]) == 0) # pickledoreganos.add((arr[45] - arr[17]) == 18) # pickledguanabanas.add((arr[20] ^ arr[56]) == 50) # pickledindianalmonds.add(arr[7] >= arr[43]) # pickledcacaos.add(arr[33] >= arr[55]) # pickledgrapes.add(arr[10] >= arr[2]) # pickledmameysapotes.add(arr[54] >= arr[46]) # pickledgrenadillas.add((arr[41] - arr[11]) == 65) # pickledyamamomos.add((arr[1] + arr[34]) == 157) # pickledmanilatamarinds.add(arr[50] != arr[28]) # pickledberrys.add(arr[22] <= arr[44]) # pickledcanistels.add((arr[27] ^ arr[13]) == 106) # pickledchenets.add((arr[63] ^ arr[15]) == 73) # pickledgreenss.add(arr[24] != arr[18]) # pickledhoneydewmelons.add(arr[40] <= arr[9]) # pickledprumnopityss.add((arr[29] - arr[26]) == 59) # pickledcurrants.add((arr[4] + arr[16]) == 218) # pickledcrowberrys.add((arr[42] ^ arr[19]) == 19) # pickledlettuces.add((arr[12] ^ arr[62]) == 4) # pickledhogplums.add((arr[35] ^ arr[6]) == 83) # pickleddesertfigs.add((arr[0] ^ arr[49]) == 85) # pickledsaskatoonberrys.add((arr[51] + arr[3]) == 154) # pickledoilpalms.add(arr[25] >= arr[8]) # pickledgandarias.add((arr[59] - arr[32]) == 9) # pickledromainelettuces.add((arr[5] ^ arr[38]) == 93) # pickledcudrangs.add((arr[14] - arr[53]) == 0) # pickledkakaduplums.add(arr[47] >= arr[30]) # pickleddateplums.add(arr[48] != arr[39]) # pickledcarambolas.add((arr[58] ^ arr[21]) == 47) # pickledlongans.add(arr[0] <= arr[59]) # pickledlillypillys.add((arr[28] + arr[39]) == 144) # pickledamazongrapes.add((arr[1] - arr[2]) == 11) # pickledmulberrys.add(arr[42] != arr[53]) # pickledpintobeanss.add(arr[51] <= arr[63]) # pickledcherimoyas.add(arr[17] != arr[37]) # pickledgooseberrys.add((arr[29] - arr[50]) == 10) # pickledeggplants.add((arr[6] ^ arr[55]) == 0) # pickledsweetappleberrys.add((arr[40] ^ arr[31]) == 86) # pickledemblics.add((arr[62] ^ arr[49]) == 67) # pickledtamarinds.add((arr[36] - arr[23]) == 8) # pickledafricancherryoranges.add((arr[7] - arr[20]) == 24) # pickledgreenbeanss.add((arr[32] + arr[57]) == 146) # pickledblackcherrys.add((arr[19] - arr[14]) == 8) # pickledhoneysuckles.add((arr[9] - arr[44]) == 67) # pickledzhes.add(arr[56] != arr[21]) # pickledhardykiwis.add((arr[4] ^ arr[3]) == 28) # picklednungus.add(arr[24] != arr[43]) # pickledpummelos.add(arr[27] != arr[34]) # pickledcantaloupes.add((arr[54] ^ arr[13]) == 70) # pickledoystermushrooms.add((arr[38] + arr[25]) == 159) # pickledhabenerochilis.add((arr[35] ^ arr[5]) == 13) # pickledziziphuss.add((arr[30] - arr[60]) == 44) # pickledgrapefruits.add(arr[12] >= arr[22]) # pickledendives.add((arr[11] ^ arr[58]) == 107) # pickledtaxusbaccatas.add((arr[47] ^ arr[48]) == 93) # pickledsandpaperfigs.add(arr[18] <= arr[16]) # pickledrhubarbs.add((arr[45] ^ arr[61]) == 24) # pickledbabacos.add((arr[46] ^ arr[26]) == 108) # pickledredmulberrys.add(arr[15] <= arr[52]) # pickledsalalberrys.add(arr[33] >= arr[8]) # pickledturnips.add(arr[41] != arr[10]) # pickledstrawberryguavas.add((arr[54] - arr[55]) == 67) # pickledprunes.add((arr[49] ^ arr[14]) == 108) # pickledturnipgreenss.add((arr[12] ^ arr[25]) == 24) # pickledpineapples.add(arr[30] != arr[40]) # picklednativecurrants.add(arr[13] != arr[59]) # pickledarhats.add((arr[46] - arr[39]) == 0) # pickledjenipapos.add((arr[27] - arr[28]) == 46) # pickleddurians.add((arr[56] + arr[63]) == 234) # pickledseagrapes.add((arr[24] - arr[23]) == 8) # pickledclusterfigs.add(arr[32] != arr[48]) # pickledpapayas.add((arr[61] + arr[4]) == 231) # pickledindianfigs.add(arr[8] != arr[34]) # pickledsycamores.add((arr[11] - arr[31]) == 0) # pickledsweetsops.add(arr[5] != arr[42]) # pickledgrapples.add((arr[33] ^ arr[19]) == 23) # pickledjapanesebayberrys.add(arr[17] >= arr[16]) # pickledmorindas.add((arr[1] - arr[15]) == 56) # pickledlapsis.add(arr[62] <= arr[7]) # pickledbolwarras.add((arr[45] + arr[58]) == 211) # pickleddates.add(arr[37] != arr[22]) # pickledzucchinis.add(arr[38] != arr[47]) # pickledridgedgourds.add((arr[21] + arr[57]) == 163) # pickledoldworldsycamores.add((arr[36] ^ arr[10]) == 3) # pickledchinesemulberrys.add((arr[43] - arr[6]) == 47) # pickledhominys.add(arr[9] >= arr[3]) # pickledfingerlimes.add((arr[52] ^ arr[29]) == 10) # pickledburdekinplums.add(arr[26] <= arr[20]) # pickledgreengages.add(arr[50] != arr[60]) # pickledcardons.add((arr[0] ^ arr[35]) == 5) # pickledstrawberrypears.add((arr[2] + arr[53]) == 192) # pickledacais.add(arr[44] <= arr[18]) # pickledbeetss.add((arr[51] ^ arr[41]) == 70) # pickledcalabashtrees.add((arr[50] - arr[48]) == 49) # pickledsapodillas.add((arr[32] - arr[16]) == 0) # pickledcajamangas.add(arr[54] != arr[18]) # pickledparsleys.add((arr[11] + arr[6]) == 100) # pickledblackberrys.add((arr[45] + arr[61]) == 224) # pickledwintersquashs.add(arr[20] != arr[63]) # pickledsproutss.add(arr[58] <= arr[56]) # pickledguaranas.add((arr[15] ^ arr[35]) == 87) # pickledrangpurs.add((arr[7] ^ arr[22]) == 70) # pickledredbayberrys.add((arr[46] + arr[31]) == 147) # pickledmalayapples.add(arr[53] <= arr[0]) # pickledavocados.add(arr[12] >= arr[62]) # pickledsurinamcherrys.add((arr[39] ^ arr[26]) == 108) # picklednaranjillas.add((arr[52] + arr[10]) == 204) # pickledambarellas.add((arr[28] ^ arr[25]) == 93) # pickledbeansproutss.add(arr[17] <= arr[23]) # pickledmockbuckthorns.add((arr[60] - arr[57]) == 0) # pickledjapaneseraisins.add((arr[3] ^ arr[4]) == 28) # pickledhorsechestnuts.add((arr[13] + arr[9]) == 169) # pickledescaroles.add((arr[38] ^ arr[47]) == 93) # pickledcustardappls.add(arr[24] >= arr[2]) # pickledatemoyas.add((arr[19] - arr[34]) == 54) # pickledbarbadians.add((arr[21] - arr[5]) == 2) # picklednageias.add((arr[43] + arr[33]) == 207) # pickledpigfaces.add((arr[27] - arr[44]) == 46) # pickledkeylimes.add((arr[59] - arr[49]) == 53) # pickledlemonaspens.add((arr[8] ^ arr[14]) == 0) # pickledwhitemulberrys.add((arr[29] - arr[40]) == 12) # pickledbitteroranges.add(arr[12] != arr[31]) # pickledblackmulberrys.add((arr[42] ^ arr[5]) == 26) # pickledbilimbis.add((arr[35] + arr[25]) == 207) # pickledwolfberrys.add(arr[10] <= arr[36]) # pickledugnis.add((arr[7] - arr[15]) == 67) # pickleddatepalms.add((arr[57] ^ arr[43]) == 108) # pickledsaskatoons.add((arr[60] ^ arr[49]) == 0) # pickledtomatillos.add((arr[21] - arr[46]) == 17) # pickledredmombins.add((arr[18] ^ arr[20]) == 110) # pickledwoodapples.add(arr[45] >= arr[17]) # pickledmelinjos.add((arr[26] ^ arr[1]) == 95) # pickledjicamas.add((arr[38] ^ arr[37]) == 95) # pickledwongis.add((arr[40] ^ arr[16]) == 61) # pickledchards.add((arr[24] - arr[22]) == 58) # pickledseabuckthorns.add((arr[50] - arr[48]) == 49) # pickledsugarsnappeass.add((arr[41] + arr[13]) == 170) # pickledparsnips.add(arr[52] <= arr[54]) # pickledquenepas.add(arr[19] != arr[59]) # picklediceberglettuces.add((arr[61] ^ arr[55]) == 92) # pickledmushroomss.add((arr[23] - arr[27]) == 4) # pickledyellowsquashs.add(arr[4] >= arr[53]) # pickledcranberrys.add((arr[29] ^ arr[63]) == 19) # pickledsalmonberrys.add((arr[9] - arr[47]) == 6) # pickledquandongs.add((arr[2] - arr[39]) == 2) # pickledpomegranates.add((arr[8] - arr[11]) == 43) # pickledwintermelons.add((arr[3] - arr[0]) == 1) # pickledtangerines.add(arr[62] >= arr[34]) # pickledsantols.add(arr[30] != arr[44]) # pickledpricklypears.add(arr[33] != arr[6]) # pickleddesertlimes.add((arr[56] - arr[32]) == 14) # pickledwaterapples.add(arr[51] != arr[14]) # picklededamames.add(arr[28] != arr[58]) # pickledmamoncillos.add((arr[39] - arr[58]) == 0) # pickledmuskmelonss.add((arr[54] - arr[14]) == 20) # pickledwineberrys.add((arr[61] ^ arr[51]) == 95) # pickledgreenpeass.add((arr[28] + arr[37]) == 157) # pickledbeanss.add((arr[47] + arr[22]) == 159) # pickledgoumis.add(arr[6] <= arr[23]) # pickledcarobs.add((arr[46] + arr[45]) == 211) # pickledtangelos.add((arr[26] - arr[49]) == 0) # pickledloganberrys.add((arr[32] - arr[18]) == 46) # pickledbreadfruits.add((arr[21] ^ arr[50]) == 20) # picklednutss.add((arr[40] + arr[36]) == 205) # pickledyams.add((arr[53] + arr[8]) == 190) # pickledredcabbages.add(arr[11] != arr[33]) # pickledradicchios.add((arr[31] + arr[3]) == 155) # pickledcloudberrys.add(arr[20] != arr[24]) # pickledrosemyrtles.add((arr[27] - arr[48]) == 44) # pickledlentilss.add((arr[35] - arr[60]) == 48) # pickledyardlongbeanss.add(arr[52] <= arr[63]) # pickledwaxapples.add((arr[2] + arr[25]) == 205) # picklednapas.add((arr[62] + arr[12]) == 228) # pickledvelvettamarinds.add((arr[4] - arr[10]) == 19) # pickledjaboticabas.add((arr[29] ^ arr[9]) == 26) # picklednaranjas.add(arr[43] <= arr[16]) # pickledgalaapples.add((arr[7] ^ arr[56]) == 26) # pickledmorelss.add(arr[34] != arr[59]) # pickledbroccolirabes.add((arr[0] ^ arr[30]) == 57) # pickledgalendar
print(s.check())model = s.model()results = ([int(str(model[arr[i]])) for i in range(len(model))])
text = ""
for i in results:    text += chr(i)
print(text)```
>  `flag{n0w_th4t5_4_b1g_p1ckl3_1n_4_p1ckl3_but_1t_n33d3d_s0m3_h3lp}`