# Boxed
After analysing the binary, I noticed the binary packed with PyInstaller.I used pyinstxtractor to extract it.```$ python pyinstxtractor.py boxed```
You will get `boxed_extracted` folder.In this folder there is .pyc files. one of them is the main file for the challenge. `main.pyc`
I used Decompyle++ tool to decompile the file and the result was:```pycdc main.pyc# Source Generated with Decompyle++# File: main.pyc (Python 3.10)import numpy as npimport boxdef main():     try:        inp = input("What's the flag? ").encode()        inp = np.array(list(inp), np.float64)        if inp.size != box.size():            print('Not even close!')            raise SystemExit        if not box.check(inp):            print('Nope!')            raise SystemExit        print('hmm... that might be the flag...')    except:        passif __name__ == '__main__':    main()```As you see our input will convert to `np.array` and there is two functions in box library `box.size()` and `box.check(inp)`, we have to check them.In boxed_extracted I found `box` library with name `box.cpython-310-x86_64-linux-gnu.so`.So, I opened `box.cpython-310-x86_64-linux-gnu.so` with IDA to analyse it.I searched in the functions list with keywords `size` and `check` and found `box.size()` function return the flag size only.```.text:00007FF1CB1F51E0 _ZN8__main__9size_2418B32c8tJTC_2fWQMSNLSg2gb4pKgGzNAE_3dE proc near.text:00007FF1CB1F51E0                                         ; CODE XREF: __pycc_method_size+3A↓p.text:00007FF1CB1F51E0                                         ; cfunc__ZN8__main__9size_2418B32c8tJTC_2fWQMSNLSg2gb4pKgGzNAE_3dE+C↓p.text:00007FF1CB1F51E0                 mov     qword ptr [rdi], 1Ah.text:00007FF1CB1F51E7                 retn.text:00007FF1CB1F51E7 _ZN8__main__9size_2418B32c8tJTC_2fWQMSNLSg2gb4pKgGzNAE_3dE endp```
The flag size is 0x1A == 26 .
In the `box.check(inp)` it should receive our input as np.array then make some calculations to find the input was correct or not.```.text:00007FF1CB1F4BF0 _ZN8__main__9check_241B32c8tJTC_2fWQMSNLSg2gb4pKgGzNAE_3dE5ArrayIdLi1E1A7mutable7alignedE proc near....[cut]....text:00007FF1CB1F4CB1                 lea     rbx, big_array.text:00007FF1CB1F4CB8                 lea     rdi, [rsp+88h+var_68] ; int.text:00007FF1CB1F4CBD                 lea     rsi, [rsp+88h+var_78] ; int.text:00007FF1CB1F4CC2                 mov     r8d, 1EEh       ; int.text:00007FF1CB1F4CC8                 mov     r9d, 8          ; int.text:00007FF1CB1F4CCE                 mov     edx, 0          ; int.text:00007FF1CB1F4CD3                 mov     ecx, 0          ; int.text:00007FF1CB1F4CD8                 push    8.text:00007FF1CB1F4CDA                 push    r14             ; __int64.text:00007FF1CB1F4CDC                 push    rax             ; x.text:00007FF1CB1F4CDD                 push    8               ; int.text:00007FF1CB1F4CDF                 push    r14             ; int.text:00007FF1CB1F4CE1                 push    0               ; int.text:00007FF1CB1F4CE3                 push    r12             ; __int64.text:00007FF1CB1F4CE5                 push    8               ; int.text:00007FF1CB1F4CE7                 push    0D0h            ; int.text:00007FF1CB1F4CEC                 push    1Ah             ; lda.text:00007FF1CB1F4CEE                 push    13h             ; n.text:00007FF1CB1F4CF0                 push    rbx             ; a.text:00007FF1CB1F4CF1                 call    _ZN5numba2np6linalg8dot_2_mv12_3clocals_3e13dot_impl_2412B44c8tJTC_2fWQA9HW1CcAv0EjzIkAdRogEkUlYBZmgA_3dE5ArrayIdLi2E1C8readonly7alignedE5ArrayIdLi1E1C7mutable7alignedE ; numba::np::linalg::dot_2_mv::_3clocals_3e::dot_impl_2412(Array<double,2,C,readonly,aligned>,Array<double,1,C,mutable,aligned>).text:00007FF1CB1F4CF6                 add     rsp, 60h....[cut]....text:00007FF1CB1F4D61                 lea     r8, final_array.text:00007FF1CB1F4D68                 cmp     rsi, r8.text:00007FF1CB1F4D6B                 setnbe  dil.text:00007FF1CB1F4D6F                 xor     esi, esi.text:00007FF1CB1F4D71                 test    r9b, r10b.text:00007FF1CB1F4D74                 jnz     loc_7FF1CB1F4E5E.text:00007FF1CB1F4D7A                 and     dl, dil.text:00007FF1CB1F4D7D                 jnz     loc_7FF1CB1F4E5E.text:00007FF1CB1F4D83                 movupd  xmm0, xmmword ptr [r14].text:00007FF1CB1F4D88                 movupd  xmm5, xmmword ptr [r14+10h].text:00007FF1CB1F4D8E                 movupd  xmm1, xmmword ptr [r14+20h].text:00007FF1CB1F4D94                 movupd  xmm7, xmmword ptr [r14+30h].text:00007FF1CB1F4D9A                 movupd  xmm2, xmmword ptr [r14+40h].text:00007FF1CB1F4DA0                 movupd  xmm6, xmmword ptr [r14+50h].text:00007FF1CB1F4DA6                 movupd  xmm3, xmmword ptr [r14+60h].text:00007FF1CB1F4DAC                 movupd  xmm4, xmmword ptr [r14+70h].text:00007FF1CB1F4DB2                 cmpeqpd xmm5, xmmword ptr cs:qword_7FF1CB208000.text:00007FF1CB1F4DBB                 cmpeqpd xmm0, xmmword ptr cs:qword_7FF1CB208000+10h....[cut]....text:00007FF1CB1F4F24 _ZN8__main__9check_241B32c8tJTC_2fWQMSNLSg2gb4pKgGzNAE_3dE5ArrayIdLi1E1A7mutable7alignedE endp```
I noticed the library use numba function `dot_2_mv` to multiply the input_array with a big_array and comparing the result with the final_array.
After googleing I found `dot_2_mv` is equivelant to `numpy.dot`.So, I decided to extract the data in the big_array and final_array.The big_array was with 494 items and because the input_array type was np.float64, I jumped to the big_array address and convert it's data to float64.and this is the result```.rodata:00007FF1CB208118 ; double big_array[494].rodata:00007FF1CB208118 big_array       dq 160.0, 477.0, 197.0, 699.0, 883.0, 300.0, 799.0, 113.0, 159.0, 288.0, 833.0, 489.0, 782.0, 895.0, 603.0, 723.0, 327.0, 129.0, 622.0.rodata:00007FF1CB208118                 dq 376.0, 664.0, 487.0, 841.0, 512.0, 382.0, 625.0, 656.0, 813.0, 329.0, 934.0, 650.0, 559.0, 421.0, 769.0, 345.0, 666.0, 107.0, 779.0.rodata:00007FF1CB208118                 dq 948.0, 141.0, 126.0, 958.0, 647.0, 576.0, 252.0, 297.0, 418.0, 602.0, 800.0, 174.0, 532.0, 287.0, 172.0, 411.0, 516.0, 780.0, 104.0.rodata:00007FF1CB208118                 dq 669.0, 524.0, 696.0, 735.0, 754.0, 654.0, 947.0, 982.0, 195.0, 453.0, 260.0, 860.0, 401.0, 132.0, 262.0, 506.0, 895.0, 297.0, 529.0.rodata:00007FF1CB208118                 dq 961.0, 689.0, 343.0, 881.0, 679.0, 350.0, 877.0, 514.0, 915.0, 323.0, 863.0, 583.0, 622.0, 748.0, 886.0, 934.0, 575.0, 202.0, 843.0.rodata:00007FF1CB208118                 dq 691.0, 809.0, 480.0, 119.0, 155.0, 655.0, 289.0, 740.0, 543.0, 566.0, 191.0, 639.0, 444.0, 855.0, 363.0, 963.0, 797.0, 613.0, 720.0.rodata:00007FF1CB208118                 dq 307.0, 890.0, 475.0, 730.0, 765.0, 274.0, 344.0, 751.0, 504.0, 623.0, 961.0, 880.0, 747.0, 129.0, 262.0, 457.0, 593.0, 480.0, 156.0.rodata:00007FF1CB208118                 dq 987.0, 719.0, 115.0, 533.0, 760.0, 108.0, 747.0, 880.0, 726.0, 474.0, 749.0, 874.0, 475.0, 735.0, 435.0, 421.0, 126.0, 270.0, 949.0.rodata:00007FF1CB208118                 dq 311.0, 359.0, 398.0, 514.0, 299.0, 473.0, 542.0, 656.0, 279.0, 793.0, 618.0, 707.0, 504.0, 356.0, 920.0, 432.0, 605.0, 917.0, 410.0.rodata:00007FF1CB208118                 dq 233.0, 772.0, 989.0, 892.0, 107.0, 179.0, 335.0, 737.0, 636.0, 392.0, 453.0, 791.0, 420.0, 553.0, 949.0, 834.0, 669.0, 690.0, 692.0.rodata:00007FF1CB208118                 dq 824.0, 564.0, 461.0, 966.0, 422.0, 589.0, 359.0, 599.0, 285.0, 949.0, 703.0, 263.0, 608.0, 772.0, 871.0, 890.0, 143.0, 237.0, 944.0.rodata:00007FF1CB208118                 dq 728.0, 682.0, 798.0, 929.0, 833.0, 737.0, 407.0, 210.0, 347.0, 703.0, 546.0, 710.0, 481.0, 919.0, 986.0, 204.0, 818.0, 611.0, 144.0.rodata:00007FF1CB208118                 dq 908.0, 643.0, 802.0, 612.0, 565.0, 746.0, 609.0, 803.0, 343.0, 833.0, 214.0, 923.0, 592.0, 186.0, 191.0, 837.0, 476.0, 155.0, 289.0.rodata:00007FF1CB208118                 dq 406.0, 267.0, 615.0, 532.0, 337.0, 576.0, 706.0, 902.0, 778.0, 857.0, 867.0, 649.0, 449.0, 833.0, 803.0, 839.0, 892.0, 902.0, 430.0.rodata:00007FF1CB208118                 dq 584.0, 842.0, 160.0, 247.0, 982.0, 765.0, 634.0, 302.0, 554.0, 896.0, 269.0, 391.0, 908.0, 749.0, 500.0, 728.0, 854.0, 279.0, 654.0.rodata:00007FF1CB208118                 dq 814.0, 232.0, 403.0, 245.0, 976.0, 163.0, 764.0, 463.0, 911.0, 533.0, 685.0, 124.0, 716.0, 441.0, 931.0, 427.0, 882.0, 224.0, 892.0.rodata:00007FF1CB208118                 dq 141.0, 563.0, 760.0, 841.0, 604.0, 605.0, 635.0, 740.0, 874.0, 382.0, 149.0, 376.0, 613.0, 137.0, 932.0, 186.0, 742.0, 921.0, 697.0.rodata:00007FF1CB208118                 dq 574.0, 863.0, 230.0, 103.0, 281.0, 464.0, 553.0, 169.0, 807.0, 390.0, 617.0, 936.0, 999.0, 189.0, 882.0, 439.0, 385.0, 335.0, 306.0.rodata:00007FF1CB208118                 dq 248.0, 189.0, 506.0, 738.0, 873.0, 935.0, 261.0, 355.0, 670.0, 208.0, 984.0, 669.0, 845.0, 704.0, 744.0, 902.0, 895.0, 401.0, 173.0.rodata:00007FF1CB208118                 dq 132.0, 977.0, 921.0, 710.0, 805.0, 697.0, 545.0, 423.0, 694.0, 377.0, 247.0, 195.0, 667.0, 905.0, 191.0, 355.0, 180.0, 433.0, 952.0.rodata:00007FF1CB208118                 dq 353.0, 825.0, 650.0, 739.0, 295.0, 653.0, 743.0, 986.0, 650.0, 385.0, 690.0, 408.0, 225.0, 656.0, 831.0, 851.0, 412.0, 623.0, 937.0.rodata:00007FF1CB208118                 dq 677.0, 735.0, 504.0, 167.0, 994.0, 654.0, 101.0, 991.0, 296.0, 390.0, 285.0, 784.0, 857.0, 219.0, 722.0, 880.0, 424.0, 463.0, 827.0.rodata:00007FF1CB208118                 dq 806.0, 345.0, 511.0, 146.0, 307.0, 498.0, 962.0, 533.0, 857.0, 641.0, 720.0, 613.0, 836.0, 770.0, 583.0, 319.0, 382.0, 575.0, 809.0.rodata:00007FF1CB208118                 dq 515.0, 466.0, 231.0, 784.0, 815.0, 109.0, 148.0, 908.0, 572.0, 241.0, 159.0, 810.0, 495.0, 405.0, 645.0, 899.0, 645.0, 891.0, 350.0.rodata:00007FF1CB208118                 dq 385.0, 480.0, 155.0, 379.0, 501.0, 454.0, 416.0, 848.0, 358.0, 402.0, 424.0, 477.0, 859.0, 854.0, 752.0, 492.0, 790.0, 201.0, 227.0.rodata:00007FF1CB208118                 dq 973.0, 312.0, 567.0, 459.0, 239.0, 449.0, 422.0, 948.0, 119.0, 261.0, 787.0, 925.0, 181.0, 310.0, 918.0, 766.0, 727.0, 175.0, 809.0```
Also the final_array was 19 items, and convert it to float64.```.rodata:00007FF1CB209088 ; double final_array[19].rodata:00007FF1CB209088 final_array     dq 1256330.0, 1339998.0, 1346424.0, 1447434.0, 1500836.0.rodata:00007FF1CB209088                 dq 1343196.0, 1341708.0, 1585556.0, 1653047.0, 1365749.0.rodata:00007FF1CB209088                 dq 1648449.0, 1500874.0, 1335251.0, 1379725.0, 1399574.0.rodata:00007FF1CB209088                 dq 1467166.0, 1487079.0, 1178725.0, 1419771.0```
Now, here is our arguments size:flag_array:   26 big_array:    494final_array:  19
To solve this math puzzle, we need to reshape the big_array to be in 2D-dimension (19x26) and also need to get the inverse array of the big_array.
I programmed a small python script to achive that but unfortunatly the result wasn't correct.```import numpy as npfinal_array = np.array([	1256330.0, 1339998.0, 1346424.0, 1447434.0,	1500836.0, 1343196.0, 1341708.0, 1585556.0,	1653047.0, 1365749.0, 1648449.0, 1500874.0,	1335251.0, 1379725.0, 1399574.0, 1467166.0,	1487079.0, 1178725.0, 1419771.0], np.float64)big_array = np.array([[160.0, 477.0, 197.0, 699.0, 883.0, 300.0, 799.0, 113.0, 159.0, 288.0, 833.0, 489.0, 782.0, 895.0, 603.0, 723.0, 327.0, 129.0, 622.0],[376.0, 664.0, 487.0, 841.0, 512.0, 382.0, 625.0, 656.0, 813.0, 329.0, 934.0, 650.0, 559.0, 421.0, 769.0, 345.0, 666.0, 107.0, 779.0],[948.0, 141.0, 126.0, 958.0, 647.0, 576.0, 252.0, 297.0, 418.0, 602.0, 800.0, 174.0, 532.0, 287.0, 172.0, 411.0, 516.0, 780.0, 104.0],[669.0, 524.0, 696.0, 735.0, 754.0, 654.0, 947.0, 982.0, 195.0, 453.0, 260.0, 860.0, 401.0, 132.0, 262.0, 506.0, 895.0, 297.0, 529.0],[961.0, 689.0, 343.0, 881.0, 679.0, 350.0, 877.0, 514.0, 915.0, 323.0, 863.0, 583.0, 622.0, 748.0, 886.0, 934.0, 575.0, 202.0, 843.0],[691.0, 809.0, 480.0, 119.0, 155.0, 655.0, 289.0, 740.0, 543.0, 566.0, 191.0, 639.0, 444.0, 855.0, 363.0, 963.0, 797.0, 613.0, 720.0],[307.0, 890.0, 475.0, 730.0, 765.0, 274.0, 344.0, 751.0, 504.0, 623.0, 961.0, 880.0, 747.0, 129.0, 262.0, 457.0, 593.0, 480.0, 156.0],[987.0, 719.0, 115.0, 533.0, 760.0, 108.0, 747.0, 880.0, 726.0, 474.0, 749.0, 874.0, 475.0, 735.0, 435.0, 421.0, 126.0, 270.0, 949.0],[311.0, 359.0, 398.0, 514.0, 299.0, 473.0, 542.0, 656.0, 279.0, 793.0, 618.0, 707.0, 504.0, 356.0, 920.0, 432.0, 605.0, 917.0, 410.0],[233.0, 772.0, 989.0, 892.0, 107.0, 179.0, 335.0, 737.0, 636.0, 392.0, 453.0, 791.0, 420.0, 553.0, 949.0, 834.0, 669.0, 690.0, 692.0],[824.0, 564.0, 461.0, 966.0, 422.0, 589.0, 359.0, 599.0, 285.0, 949.0, 703.0, 263.0, 608.0, 772.0, 871.0, 890.0, 143.0, 237.0, 944.0],[728.0, 682.0, 798.0, 929.0, 833.0, 737.0, 407.0, 210.0, 347.0, 703.0, 546.0, 710.0, 481.0, 919.0, 986.0, 204.0, 818.0, 611.0, 144.0],[908.0, 643.0, 802.0, 612.0, 565.0, 746.0, 609.0, 803.0, 343.0, 833.0, 214.0, 923.0, 592.0, 186.0, 191.0, 837.0, 476.0, 155.0, 289.0],[406.0, 267.0, 615.0, 532.0, 337.0, 576.0, 706.0, 902.0, 778.0, 857.0, 867.0, 649.0, 449.0, 833.0, 803.0, 839.0, 892.0, 902.0, 430.0],[584.0, 842.0, 160.0, 247.0, 982.0, 765.0, 634.0, 302.0, 554.0, 896.0, 269.0, 391.0, 908.0, 749.0, 500.0, 728.0, 854.0, 279.0, 654.0],[814.0, 232.0, 403.0, 245.0, 976.0, 163.0, 764.0, 463.0, 911.0, 533.0, 685.0, 124.0, 716.0, 441.0, 931.0, 427.0, 882.0, 224.0, 892.0],[141.0, 563.0, 760.0, 841.0, 604.0, 605.0, 635.0, 740.0, 874.0, 382.0, 149.0, 376.0, 613.0, 137.0, 932.0, 186.0, 742.0, 921.0, 697.0],[574.0, 863.0, 230.0, 103.0, 281.0, 464.0, 553.0, 169.0, 807.0, 390.0, 617.0, 936.0, 999.0, 189.0, 882.0, 439.0, 385.0, 335.0, 306.0],[248.0, 189.0, 506.0, 738.0, 873.0, 935.0, 261.0, 355.0, 670.0, 208.0, 984.0, 669.0, 845.0, 704.0, 744.0, 902.0, 895.0, 401.0, 173.0],[132.0, 977.0, 921.0, 710.0, 805.0, 697.0, 545.0, 423.0, 694.0, 377.0, 247.0, 195.0, 667.0, 905.0, 191.0, 355.0, 180.0, 433.0, 952.0],[353.0, 825.0, 650.0, 739.0, 295.0, 653.0, 743.0, 986.0, 650.0, 385.0, 690.0, 408.0, 225.0, 656.0, 831.0, 851.0, 412.0, 623.0, 937.0],[677.0, 735.0, 504.0, 167.0, 994.0, 654.0, 101.0, 991.0, 296.0, 390.0, 285.0, 784.0, 857.0, 219.0, 722.0, 880.0, 424.0, 463.0, 827.0],[806.0, 345.0, 511.0, 146.0, 307.0, 498.0, 962.0, 533.0, 857.0, 641.0, 720.0, 613.0, 836.0, 770.0, 583.0, 319.0, 382.0, 575.0, 809.0],[515.0, 466.0, 231.0, 784.0, 815.0, 109.0, 148.0, 908.0, 572.0, 241.0, 159.0, 810.0, 495.0, 405.0, 645.0, 899.0, 645.0, 891.0, 350.0],[385.0, 480.0, 155.0, 379.0, 501.0, 454.0, 416.0, 848.0, 358.0, 402.0, 424.0, 477.0, 859.0, 854.0, 752.0, 492.0, 790.0, 201.0, 227.0],[973.0, 312.0, 567.0, 459.0, 239.0, 449.0, 422.0, 948.0, 119.0, 261.0, 787.0, 925.0, 181.0, 310.0, 918.0, 766.0, 727.0, 175.0, 809.0]], np.float64)big_array = big_array.reshape(19, 26)# big_array_inv = np.linalg.inv(big_array) # it raise error because the big_array is not a squared array.big_array_inv = np.linalg.pinv(big_array)result = big_array_inv.dot(final_array)result = result.astype(int)print(''.join([chr(c) for c in result]))```
The result: `|nbh\XD}hMbx-ySl5t2dintESp`
WHY !!!!
After googleing I figured out that the big_array is not a squared array,and for this reason I can't use `np.linalg.inv` and instead I used `np.linalg.pinv`and because the function `np.linalg.pinv` return the nearest inverse for the target matrix, the result was not correct.
At this moment I decided to use z3 Solver and here is my final python script:
```import numpy as npfrom z3 import Solver, BitVec, sata = np.array([    1256330.0, 1339998.0, 1346424.0, 1447434.0,    1500836.0, 1343196.0, 1341708.0, 1585556.0,    1653047.0, 1365749.0, 1648449.0, 1500874.0,    1335251.0, 1379725.0, 1399574.0, 1467166.0,    1487079.0, 1178725.0, 1419771.0], np.float64)b = np.array([[160.0, 477.0, 197.0, 699.0, 883.0, 300.0, 799.0, 113.0, 159.0, 288.0, 833.0, 489.0, 782.0, 895.0, 603.0, 723.0, 327.0, 129.0, 622.0],[376.0, 664.0, 487.0, 841.0, 512.0, 382.0, 625.0, 656.0, 813.0, 329.0, 934.0, 650.0, 559.0, 421.0, 769.0, 345.0, 666.0, 107.0, 779.0],[948.0, 141.0, 126.0, 958.0, 647.0, 576.0, 252.0, 297.0, 418.0, 602.0, 800.0, 174.0, 532.0, 287.0, 172.0, 411.0, 516.0, 780.0, 104.0],[669.0, 524.0, 696.0, 735.0, 754.0, 654.0, 947.0, 982.0, 195.0, 453.0, 260.0, 860.0, 401.0, 132.0, 262.0, 506.0, 895.0, 297.0, 529.0],[961.0, 689.0, 343.0, 881.0, 679.0, 350.0, 877.0, 514.0, 915.0, 323.0, 863.0, 583.0, 622.0, 748.0, 886.0, 934.0, 575.0, 202.0, 843.0],[691.0, 809.0, 480.0, 119.0, 155.0, 655.0, 289.0, 740.0, 543.0, 566.0, 191.0, 639.0, 444.0, 855.0, 363.0, 963.0, 797.0, 613.0, 720.0],[307.0, 890.0, 475.0, 730.0, 765.0, 274.0, 344.0, 751.0, 504.0, 623.0, 961.0, 880.0, 747.0, 129.0, 262.0, 457.0, 593.0, 480.0, 156.0],[987.0, 719.0, 115.0, 533.0, 760.0, 108.0, 747.0, 880.0, 726.0, 474.0, 749.0, 874.0, 475.0, 735.0, 435.0, 421.0, 126.0, 270.0, 949.0],[311.0, 359.0, 398.0, 514.0, 299.0, 473.0, 542.0, 656.0, 279.0, 793.0, 618.0, 707.0, 504.0, 356.0, 920.0, 432.0, 605.0, 917.0, 410.0],[233.0, 772.0, 989.0, 892.0, 107.0, 179.0, 335.0, 737.0, 636.0, 392.0, 453.0, 791.0, 420.0, 553.0, 949.0, 834.0, 669.0, 690.0, 692.0],[824.0, 564.0, 461.0, 966.0, 422.0, 589.0, 359.0, 599.0, 285.0, 949.0, 703.0, 263.0, 608.0, 772.0, 871.0, 890.0, 143.0, 237.0, 944.0],[728.0, 682.0, 798.0, 929.0, 833.0, 737.0, 407.0, 210.0, 347.0, 703.0, 546.0, 710.0, 481.0, 919.0, 986.0, 204.0, 818.0, 611.0, 144.0],[908.0, 643.0, 802.0, 612.0, 565.0, 746.0, 609.0, 803.0, 343.0, 833.0, 214.0, 923.0, 592.0, 186.0, 191.0, 837.0, 476.0, 155.0, 289.0],[406.0, 267.0, 615.0, 532.0, 337.0, 576.0, 706.0, 902.0, 778.0, 857.0, 867.0, 649.0, 449.0, 833.0, 803.0, 839.0, 892.0, 902.0, 430.0],[584.0, 842.0, 160.0, 247.0, 982.0, 765.0, 634.0, 302.0, 554.0, 896.0, 269.0, 391.0, 908.0, 749.0, 500.0, 728.0, 854.0, 279.0, 654.0],[814.0, 232.0, 403.0, 245.0, 976.0, 163.0, 764.0, 463.0, 911.0, 533.0, 685.0, 124.0, 716.0, 441.0, 931.0, 427.0, 882.0, 224.0, 892.0],[141.0, 563.0, 760.0, 841.0, 604.0, 605.0, 635.0, 740.0, 874.0, 382.0, 149.0, 376.0, 613.0, 137.0, 932.0, 186.0, 742.0, 921.0, 697.0],[574.0, 863.0, 230.0, 103.0, 281.0, 464.0, 553.0, 169.0, 807.0, 390.0, 617.0, 936.0, 999.0, 189.0, 882.0, 439.0, 385.0, 335.0, 306.0],[248.0, 189.0, 506.0, 738.0, 873.0, 935.0, 261.0, 355.0, 670.0, 208.0, 984.0, 669.0, 845.0, 704.0, 744.0, 902.0, 895.0, 401.0, 173.0],[132.0, 977.0, 921.0, 710.0, 805.0, 697.0, 545.0, 423.0, 694.0, 377.0, 247.0, 195.0, 667.0, 905.0, 191.0, 355.0, 180.0, 433.0, 952.0],[353.0, 825.0, 650.0, 739.0, 295.0, 653.0, 743.0, 986.0, 650.0, 385.0, 690.0, 408.0, 225.0, 656.0, 831.0, 851.0, 412.0, 623.0, 937.0],[677.0, 735.0, 504.0, 167.0, 994.0, 654.0, 101.0, 991.0, 296.0, 390.0, 285.0, 784.0, 857.0, 219.0, 722.0, 880.0, 424.0, 463.0, 827.0],[806.0, 345.0, 511.0, 146.0, 307.0, 498.0, 962.0, 533.0, 857.0, 641.0, 720.0, 613.0, 836.0, 770.0, 583.0, 319.0, 382.0, 575.0, 809.0],[515.0, 466.0, 231.0, 784.0, 815.0, 109.0, 148.0, 908.0, 572.0, 241.0, 159.0, 810.0, 495.0, 405.0, 645.0, 899.0, 645.0, 891.0, 350.0],[385.0, 480.0, 155.0, 379.0, 501.0, 454.0, 416.0, 848.0, 358.0, 402.0, 424.0, 477.0, 859.0, 854.0, 752.0, 492.0, 790.0, 201.0, 227.0],[973.0, 312.0, 567.0, 459.0, 239.0, 449.0, 422.0, 948.0, 119.0, 261.0, 787.0, 925.0, 181.0, 310.0, 918.0, 766.0, 727.0, 175.0, 809.0]]], np.float64)f = []sol = Solver()for i in range(26):    f.append(BitVec('f%2d' % i, 32))    if i not in [0, 1, 2, 3, 4, 5, 25]:        sol.add(f[i] > 0x2f, f[i] < 0x7b)        for j in range(0x3a, 0x41): # exclude chars             sol.add(f[i] != j)# add the characters I know in the flagsol.add(f[0] == ord('t'))sol.add(f[1] == ord('j'))sol.add(f[2] == ord('c'))sol.add(f[3] == ord('t'))sol.add(f[4] == ord('f'))sol.add(f[5] == ord('{'))sol.add(f[25] == ord('}'))b = b.reshape(19, 26)a = list(map(int, a)) # convert float values to integer for final_arrayfor j in range(19):    c = b[j,:] # get a row values    c = list(map(int, c)) # convert float values to integer    sum1 = 0    for i in range(26):        sum1 += c[i] * f[i]    sol.add(sum1 == a[j])# https://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation/70656700#70656700def all_smt(s, initial_terms):    def block_term(s, m, t):        s.add(t != m.eval(t, model_completion=True))    def fix_term(s, m, t):        s.add(t == m.eval(t, model_completion=True))    def all_smt_rec(terms):        if sat == s.check():            m = s.model()            yield m            for i in range(len(terms)):                s.push()                block_term(s, m, terms[i])                for j in range(i):                    fix_term(s, m, terms[j])                yield from all_smt_rec(terms[i:])                s.pop()    yield from all_smt_rec(list(initial_terms)) for m in all_smt(sol, f):    flag = ''    for i in f:        flag += chr(m[i].as_long())    print(flag)    exit()```
Here is the flag: `tjctf{1ts_ju5t_l1n3s_lm40}`