## Write-up DiceCTF 2025 (Reversing strategy)
> Tbh, i dedicated lots of time and effort to this contest. In the end, i solved 3 problems and my team secured a quite good place among all teams. I don't think this contest has overly easy reversing challenges, so thanks to myself for staying consistent!
### 1. Debugalyzer
- Alright, starting with the first reversing challenge, we have a total of two files to work with.
- I want to focus more on exploring inside dwarf first so it's time to dive into ida.

- After analyzing the pseudocode for a while, I realized that it primarily calculates and prints information about the file provided as an argument (in this case, the file 'main') and the function we likely need to focus on the most is **execute_dwarf_bytecode_v4**
- Meanwhile when open file **main**, there's still nothing special there:
- After a closer inspection and some debugging, i discovered that the function **execute_dwarf_bytecode_v4** operates like a VM with its own set of opcodes.
- In general, I discovered that in our real opcodes of this challenge include 2 main kinds of instructions which start with either 82 or 81:
- These are some typical instructions begin with opcode 81:
- It's likely that an array is created based on the intruction pattern as follows:
+ The value of each element is determined by the third byte of the opcode.
+ The index of each element is determined by the third byte of the opcode.

- And these are some typical instructions begin with opcode 82:

- It looks like more complicated than 81 right! but if we observant how the program deals with it, it won't be too difficult to realize that the 2nd and 3rd byte of an instruction are the index, byte 4th will be the mode (there's totally 4 modes).
- 0 - Add
- 1 - Subtract
- 2 - Multiply
- 3 - XOR
- Byte 5th will be the expected result.
- From this point, we can see the complete picture of our challenge: our task is to identify an array that meets certain specific constraints.
- This is my python script using z3:

from z3 import *

v = [BitVec(f'v{i}', 8) for i in range(40)]

solver = Solver()

solver.add(v[0] == ord('d'))
solver.add(v[1] == ord('i'))
solver.add(v[2] == ord('c'))
solver.add(v[3] == ord('e'))
solver.add(v[4] == ord('{'))
solver.add(v[39] == ord('}'))


patterns = [(82, 0, 19, 1, 247, 0, 5),
(82, 0, 23, 1, 48, 0, 5),
(82, 0, 28, 3, 19, 0, 5),
(82, 0, 22, 0, 149, 0, 5),
(82, 0, 36, 3, 23, 0, 5),
(82, 1, 25, 1, 245, 0, 5),
(82, 1, 37, 3, 90, 0, 5),
(82, 1, 15, 0, 204, 0, 5),
(82, 1, 22, 3, 88, 0, 5),
(82, 1, 30, 0, 219, 0, 5),
(82, 2, 16, 2, 189, 0, 5),
(82, 2, 10, 2, 203, 0, 5),
(82, 2, 27, 1, 255, 0, 5),
(82, 2, 32, 0, 194, 0, 5),
(82, 2, 24, 3, 13, 0, 5),
(82, 3, 31, 2, 62, 0, 5),
(82, 3, 27, 0, 201, 0, 5),
(82, 3, 11, 2, 123, 0, 5),
(82, 3, 6, 0, 150, 0, 5),
(82, 3, 21, 2, 156, 0, 5),
(82, 4, 17, 2, 145, 0, 5),
(82, 4, 5, 1, 19, 0, 5),
(82, 4, 35, 0, 237, 0, 5),
(82, 4, 36, 3, 8, 0, 5),
(82, 4, 8, 2, 248, 0, 5),
(82, 5, 8, 0, 208, 0, 5),
(82, 5, 26, 1, 9, 0, 5),
(82, 5, 21, 1, 252, 0, 5),
(82, 5, 14, 2, 184, 0, 5),
(82, 5, 36, 0, 219, 0, 5),
(82, 6, 0, 2, 36, 0, 5),
(82, 6, 24, 0, 159, 0, 5),
(82, 6, 34, 0, 101, 0, 5),
(82, 6, 21, 1, 197, 0, 5),
(82, 6, 13, 3, 65, 0, 5),
(82, 7, 23, 0, 155, 0, 5),
(82, 7, 1, 1, 254, 0, 5),
(82, 7, 38, 3, 21, 0, 5),
(82, 7, 16, 0, 198, 0, 5),
(82, 7, 30, 3, 21, 0, 5),
(82, 8, 0, 3, 12, 0, 5),
(82, 8, 38, 0, 218, 0, 5),
(82, 8, 27, 3, 12, 0, 5),
(82, 8, 23, 1, 52, 0, 5),
(82, 8, 9, 1, 252, 0, 5),
(82, 9, 9, 1, 0, 0, 5),
(82, 9, 35, 3, 30, 0, 5),
(82, 9, 25, 1, 248, 0, 5),
(82, 9, 34, 3, 88, 0, 5),
(82, 9, 32, 1, 13, 0, 5),
(82, 10, 22, 1, 72, 0, 5),
(82, 10, 8, 1, 17, 0, 5),
(82, 10, 25, 3, 13, 0, 5),
(82, 10, 14, 1, 70, 0, 5),
(82, 10, 29, 1, 69, 0, 5),
(82, 11, 0, 3, 59, 0, 5),
(82, 11, 32, 0, 190, 0, 5),
(82, 11, 19, 0, 204, 0, 5),
(82, 11, 35, 0, 209, 0, 5),
(82, 11, 14, 2, 237, 0, 5),
(82, 12, 13, 0, 227, 0, 5),
(82, 12, 11, 1, 20, 0, 5),
(82, 12, 25, 1, 255, 0, 5),
(82, 12, 20, 0, 227, 0, 5),
(82, 12, 6, 3, 66, 0, 5),
(82, 13, 36, 3, 3, 0, 5),
(82, 13, 5, 3, 24, 0, 5),
(82, 13, 2, 3, 19, 0, 5),
(82, 13, 6, 1, 63, 0, 5),
(82, 13, 38, 0, 226, 0, 5),
(82, 14, 6, 1, 2, 0, 5),
(82, 14, 22, 0, 100, 0, 5),
(82, 14, 36, 3, 64, 0, 5),
(82, 14, 13, 1, 195, 0, 5),
(82, 14, 12, 1, 192, 0, 5),
(82, 15, 28, 3, 20, 0, 5),
(82, 15, 13, 1, 243, 0, 5),
(82, 15, 20, 3, 19, 0, 5),
(82, 15, 34, 1, 47, 0, 5),
(82, 15, 21, 2, 196, 0, 5),
(82, 16, 17, 1, 252, 0, 5),
(82, 16, 23, 1, 43, 0, 5),
(82, 16, 37, 0, 146, 0, 5),
(82, 16, 20, 0, 207, 0, 5),
(82, 16, 5, 1, 247, 0, 5),
(82, 17, 35, 3, 17, 0, 5),
(82, 17, 29, 2, 28, 0, 5),
(82, 17, 2, 2, 73, 0, 5),
(82, 17, 16, 0, 194, 0, 5),
(82, 17, 10, 1, 234, 0, 5),
(82, 18, 22, 1, 255, 0, 5),
(82, 18, 39, 2, 112, 0, 5),
(82, 18, 20, 3, 64, 0, 5),
(82, 18, 21, 3, 92, 0, 5),
(82, 18, 35, 1, 190, 0, 5),
(82, 19, 38, 0, 223, 0, 5),
(82, 19, 35, 1, 251, 0, 5),
(82, 19, 15, 1, 10, 0, 5),
(82, 19, 18, 0, 157, 0, 5),
(82, 19, 30, 1, 251, 0, 5),
(82, 20, 7, 1, 9, 0, 5),
(82, 20, 1, 0, 217, 0, 5),
(82, 20, 17, 3, 19, 0, 5),
(82, 20, 39, 3, 13, 0, 5),
(82, 20, 16, 1, 17, 0, 5),
(82, 21, 8, 1, 4, 0, 5),
(82, 21, 1, 3, 5, 0, 5),
(82, 21, 23, 1, 56, 0, 5),
(82, 21, 3, 1, 7, 0, 5),
(82, 21, 30, 3, 30, 0, 5),
(82, 22, 27, 3, 85, 0, 5),
(82, 22, 8, 1, 201, 0, 5),
(82, 22, 23, 3, 5, 0, 5),
(82, 22, 39, 0, 174, 0, 5),
(82, 22, 18, 0, 97, 0, 5),
(82, 23, 0, 2, 80, 0, 5),
(82, 23, 24, 0, 162, 0, 5),
(82, 23, 38, 3, 70, 0, 5),
(82, 23, 34, 2, 144, 0, 5),
(82, 23, 37, 2, 92, 0, 5),
(82, 24, 6, 3, 95, 0, 5),
(82, 24, 1, 1, 5, 0, 5),
(82, 24, 35, 0, 224, 0, 5),
(82, 24, 3, 1, 9, 0, 5),
(82, 24, 11, 3, 49, 0, 5),
(82, 25, 28, 3, 3, 0, 5),
(82, 25, 30, 0, 230, 0, 5),
(82, 25, 6, 0, 165, 0, 5),
(82, 25, 3, 3, 17, 0, 5),
(82, 25, 8, 3, 28, 0, 5),
(82, 26, 10, 0, 216, 0, 5),
(82, 26, 31, 2, 218, 0, 5),
(82, 26, 35, 0, 209, 0, 5),
(82, 26, 13, 0, 207, 0, 5),
(82, 26, 23, 0, 147, 0, 5),
(82, 27, 7, 0, 203, 0, 5),
(82, 27, 20, 2, 192, 0, 5),
(82, 27, 6, 0, 149, 0, 5),
(82, 27, 30, 0, 214, 0, 5),
(82, 27, 34, 2, 80, 0, 5),
(82, 28, 31, 3, 17, 0, 5),
(82, 28, 13, 0, 231, 0, 5),
(82, 28, 30, 1, 5, 0, 5),
(82, 28, 39, 3, 10, 0, 5),
(82, 28, 5, 3, 31, 0, 5),
(82, 29, 39, 0, 177, 0, 5),
(82, 29, 32, 3, 107, 0, 5),
(82, 29, 15, 2, 28, 0, 5),
(82, 29, 24, 0, 162, 0, 5),
(82, 29, 28, 2, 44, 0, 5),
(82, 30, 24, 2, 252, 0, 5),
(82, 30, 36, 2, 54, 0, 5),
(82, 30, 27, 2, 136, 0, 5),
(82, 30, 14, 2, 182, 0, 5),
(82, 30, 30, 1, 0, 0, 5),
(82, 31, 18, 2, 32, 0, 5),
(82, 31, 33, 3, 22, 0, 5),
(82, 31, 7, 0, 205, 0, 5),
(82, 31, 29, 0, 154, 0, 5),
(82, 31, 4, 0, 225, 0, 5),
(82, 32, 34, 3, 107, 0, 5),
(82, 32, 35, 0, 209, 0, 5),
(82, 32, 2, 2, 189, 0, 5),
(82, 32, 32, 3, 0, 0, 5),
(82, 32, 18, 2, 208, 0, 5),
(82, 33, 19, 1, 3, 0, 5),
(82, 33, 12, 1, 253, 0, 5),
(82, 33, 25, 3, 4, 0, 5),
(82, 33, 16, 3, 47, 0, 5),
(82, 33, 30, 0, 226, 0, 5),
(82, 34, 7, 2, 236, 0, 5),
(82, 34, 10, 2, 148, 0, 5),
(82, 34, 2, 0, 151, 0, 5),
(82, 34, 30, 2, 40, 0, 5),
(82, 34, 15, 2, 28, 0, 5),
(82, 35, 8, 1, 10, 0, 5),
(82, 35, 16, 0, 209, 0, 5),
(82, 35, 31, 3, 20, 0, 5),
(82, 35, 9, 1, 6, 0, 5),
(82, 35, 33, 3, 2, 0, 5),
(82, 36, 15, 0, 214, 0, 5),
(82, 36, 39, 0, 240, 0, 5),
(82, 36, 10, 0, 236, 0, 5),
(82, 36, 35, 3, 1, 0, 5),
(82, 36, 4, 1, 248, 0, 5),
(82, 37, 17, 0, 150, 0, 5),
(82, 37, 8, 3, 91, 0, 5),
(82, 37, 23, 0, 103, 0, 5),
(82, 37, 36, 1, 192, 0, 5),
(82, 37, 7, 2, 133, 0, 5),
(82, 38, 13, 1, 2, 0, 5),
(82, 38, 31, 3, 20, 0, 5),
(82, 38, 39, 2, 170, 0, 5),
(82, 38, 12, 1, 255, 0, 5),
(82, 38, 28, 2, 254, 0, 5),
(82, 39, 22, 0, 174, 0, 5),
(82, 39, 24, 3, 19, 0, 5),
(82, 39, 2, 1, 26, 0, 5),
(82, 39, 30, 0, 239, 0, 5),
(82, 39, 36, 1, 10, 0, 1)]

for pattern in patterns:
    _, idx1, idx2, operation, result, _, _ = pattern

    if operation == 0:  # Add
        solver.add(v[idx1] + v[idx2] == result)
    elif operation == 1:  # Subtract
        solver.add(v[idx1] - v[idx2] == result)
    elif operation == 2:  # Multiply
        solver.add(v[idx1] * v[idx2] == result)
    elif operation == 3:  # XOR
        solver.add(v[idx1] ^ v[idx2] == result)




if solver.check() == sat:
    model = solver.model()
    print("Solution found!")
    for i in range(40):
        print(chr(model[v[i]].as_long()), end='')
else:
    print("No solution exists.")


### 2. oño
- I wanna say that ... i hate this challenge TT as it took me so long to find the flag ...
- We have to deal with only 1 elf file ... but it's actually 4 later :))
- So looking at the main function i find something suspicious there:
- First, it checks our flag's length:
- But let's take a look at the end of this if block
- Alright, if fexecve() executes successfully, puts(::s) won't execute and we may have diffirent output (not like the output i run at the first pic).

- Our question now is that how can we make it does fexecve() sucessfully?
- Based on the code above, v4 just extracts only QWORD(8 bytes) from our input string and incorporates it into some calculations. Ultimately, it generally contributes to the change of the first arg of **fexecve()**
- We all know the flag format is "dice{...}" so I just attempted to set 8 first bytes of input string to "dice{XXX" and gave it a try.

- Watching some first bytes of the program which is about to be executed by fexecve, we see something like this:
- Since the env of fexecve() derived from the file our goals become clear: 8 bytes resulting must match those values:
- 
- We have our first script to find first 8 bytes input accepted like this:

#include <stdio.h>
#include <stdint.h>
#include <string.h>
#include "defs.h"

__int64 v4,i,tmp,v5;
__int64 vtmp = 0x7F861CD6D160EBC3;
int v10;

int main()
{

    for (i = 0; i <= 0xffffff; i++)
    {
        v4 = 0x7B65636964 + (i << 40);
        tmp = v4;
        v5 = 0x4C01DB400B0C9LL * vtmp;
        v5 ^= v4;
     
        if (v5 == 0x010102464c457f)
        {
            printf("%016llx\n", tmp);

            // Extract and print each byte of tmp as a character
            for (int j = 0; j < 8; j++)
            {
                char byte = (tmp >> (j * 8)) & 0xFF; // Extract each byte
                printf("%c", byte); // Print as character
            }
            printf("\n");
        }
    }
       
    return 0;
}


- Let's dive into what does fexecve() do by decompiling its program bytecode.
- Examining the main function, we encounter a similar pattern to the original challenge file. Therefore, our goal remains the same: to ensure that executes successfully.

- By debugging it's not hard to discover that v5 is our next 8 bytes input string, so we can see in the loop that: each time it will change 8 bytes of next program bytecode, after change it keeps current position byte by stepping to the next position by 1 byte.
- Realizing that point, i wrote a z3 python script to achieve the next 8 bytes input string. (our target remains the same)

from z3 import *
arr =[0xE1, 0xAF, 0x4B, 0xDF, 0x9D, 0xC6, 0x25, 0xC1, 0xB9, 0xC9, 0xEB, 0x15, 0xC3, 0x8C, 0x00, 0x00, 0]
tpc = [0x7f, 0x45, 0x4c, 0x46, 0x02, 0x01, 0x01, 0, 0]
v = int.from_bytes(bytes(arr[0:8])[::-1], byteorder='big')

solver = Solver()
T = BitVec('T', 64)

for i in range(8):
    tmp = T * v
    solver.add(tmp & 0xff == tpc[i])
    v = tmp
    v >>= 8
    v |= (arr[8 + i] << (7 * 8))

if solver.check() == sat:
    model = solver.model()
    print("Solution for T:", bytes.fromhex(hex(model[T].as_long())[2:])[::-1])
else:
    print("No solution exists.")

    


- Since our flag is divided into 4 parts so we need to handle with 2 additional files to complete the challenge. And this is the core part of the next file:
- It's quite straightforward: We've already known v6 (v6 is calculated in the previous part) and we need to find v7 which is our next 8 bytes input string.
- It sounds like quite easy right? Howerver, the real challenge lies in v3, which holds a value derived from a overflow calculation. Ultimately, it's still solvable.

v = 0x30635f337233775f ^ 8940005473485202353
multiplier = 0x0D4308F96CA525D5A
constant = 0x7E34413175C77CE8
target = v
mod_value = 2**64

result = (target - constant) % mod_value


import math
gcd = math.gcd(multiplier, mod_value)
if result % gcd == 0:
    
    reduced_multiplier = multiplier // gcd
    reduced_mod = mod_value // gcd
    reduced_result = result // gcd
    
    inverse = pow(reduced_multiplier, -1, reduced_mod)
    
    
    T = (reduced_result * inverse) % reduced_mod
    
    
    print(bytes.fromhex(hex(T)[2:])[::-1])
    
else:
    print("No solution exists")


- Okay, let's finish this challenge with the last part!

- This time our program seems to be more complicated to reverse than 3 parts before.
- To reach our ideal puts() function we need to understand what does sub_1249() do first.
- All clues like: a2 / 8 + (* v3) or a2 % 8 + v3[1] give me the sense that i'm working on a 8x8 matrix. Additionally, it makes much sense that 8 bytes 0f input string = 8bit * 8bit)
- Take a closer look at &unk_4040:
- Not too hard to know each 8 bytes presenting for a direction right! So we totally have 4 directions: up, down, right, left.

- The fact that sub_1249 uses directions within its function and invokes itself suggests that it might be related to BFS or DFS algorithm, with specific constraints determined by the conditions in the if block.

- I spent some time to experiment with how it spreads across the matrix rather than focusing solely staticcally analyzing specific checks performed by the if conditions.

- In the end, i discover that it will spread based on the bit of current cell (1 bit for 1 cell) and it exactly spreads until it can not move more. The value which it returns is the amount of cells it visited. Examining the binary i found this:
- The numbers greater than 0 represent the count of cells must be equal with the value of sub_1249 returns when being called from this position.
- Having all necessary things, i decided to find the suitable matrix by myself. Luckily, it did not take me a lot of time.
- V5 is the matrix v15 we know before. So this is the final script to get this challenge flag:

flag = "dice{n0w_w3r3_c0oK1nG_w1"
v = hex(0xf6902caaa2aa86e0 ^ 10065931777680461460)[2:]
v = bytes.fromhex(v)
v = v[::-1]
for i in v:
    flag +=chr(i)   
print(flag)

### 3. Nonograms
- The challenge's name partly hints us about the the thing we're about to deal with:
- But the rules of this challenge appear to be quite distinctive. Our goal is to adjust color of each cell in a row/col so that the red value of that row/col matches the value of black one.
- Initially, i inspected the source code of this challenge. Since i saw a quite big wasm file, i decided to focus on examining the rules that red value changes its value first.
- First of all, i noticed that every red value on row/col will remain the same rule of changing value. i treated each cell (in a row or col) as having its own value (key value). I tried performing XOR operation between 2 key values like the screenshot above: 0xc29a ^ 0x8d2a = 0x4fb0. It seems to be in a reverse byte order when comparing this to black value. So i just change it to (~(0xc29a ^ 0x8d2a ) & 0xffff) = 0xb04f now it becomes our expected value: the black one. Fortunately, when i applied this formula for more cases it still corrects!
- So now, as we already have the the challenge rules we need to think about the way to solve it. The matrix size is significantly large enough for such a traditional brute forcing trying 0/1 for each cell becomes impossible. Understanding the influence of each cell on the entire matrix, it makes more sense to come up with z3 solver approach.

from z3 import *


expected_row = [
    0x6d5c, 0xe1f4, 0x0e05, 0x4c83, 0x801c, 0x9d09, 0xd041, 0x7680,
    0xa050, 0x2024, 0x7a61, 0x9c87, 0xf321, 0x98e0, 0x3698, 0xef35,
    0x5c48, 0x86aa, 0x80c7, 0x05be, 0xc22d, 0xb6a4, 0xf609, 0xf01a, 0x501a,
]

expected_col = [
    0xA050, 0xFFC6, 0xD3BE, 0x3249, 0xD4B7, 0x92AB, 0x9553, 0x5EAA,
    0x4A10, 0xAF30, 0x8384, 0x9AF1, 0xD098, 0xFB91, 0x1BBD, 0x55F0,
    0x58F2, 0xAD51, 0xD041, 0x494E, 0xEAF5, 0x210C, 0xC29A, 0xC1A4, 0x464F
]

key_row = [
    0xc29a, 0x8d2a, 0x5827, 0xac13, 0xd609, 0xeb04, 0x6b30, 0x2b2a,
    0x0b27, 0xe267, 0xf133, 0xf899, 0xfc4c, 0x6094, 0x2ef8, 0x09ce,
    0x1a55, 0xe8bc, 0x6aec, 0x2bc4, 0x0b50, 0x1b1a, 0x133f, 0x899f, 0xc4cf,
]


v = [BitVec(f'v{i}', 32) for i in range(25)]
solver = Solver()


for i in range(25):
    ans = BitVecVal(0xffff, 32)  
    for j in range(25):
        ans = If(Extract(j, j, v[i]) == 1, ~(ans ^ key_row[j]) & 0xffff, ans)
    solver.add(ans == expected_row[i])


for i in range(25):
    ans = BitVecVal(0xffff, 32)  
    for j in range(24, -1, -1):
        ans = If(Extract(i, i, v[j]) == 1, ~(ans ^ key_row[24 - j]) & 0xffff, ans)
    solver.add(ans == expected_col[i])

# thanh ngang dai
for i in range(18,25):
    solver.add(((v[0] >> i) & 1) == 1)
    solver.add(((v[6] >> i) & 1) == 1)   
    solver.add(((v[24] >> i) & 1) == 1) 
    solver.add(((v[18] >> i) & 1) == 1)


for i in range(7):
    solver.add(((v[0] >> i) & 1) == 1)
    solver.add(((v[6] >> i) & 1) == 1)

for i in range(1,6):
    solver.add(((v[i] >> 24) & 1) == 1)
    solver.add(((v[i] >> 18) & 1) == 1)
    solver.add(((v[i] >> 6) & 1) == 1)
    solver.add(((v[i] >> 0) & 1) == 1)

for i in range(19,24):
    solver.add(((v[i] >> 24) & 1) == 1)
    solver.add(((v[i] >> 18) & 1) == 1)

# 3 cuc o giua
for i in range(2,5):
    solver.add(((v[i] >> 22) & 1) == 1)
    solver.add(((v[i] >> 21) & 1) == 1)
    solver.add(((v[i] >> 20) & 1) == 1)
    solver.add(((v[i] >> 2) & 1) == 1)
    solver.add(((v[i] >> 3) & 1) == 1)
    solver.add(((v[i] >> 4) & 1) == 1)

for i in range(20,23):
    solver.add(((v[i] >> 22) & 1) == 1)
    solver.add(((v[i] >> 21) & 1) == 1)
    solver.add(((v[i] >> 20) & 1) == 1)
    

## add mau trang


for i in range(19,24):
    solver.add(((v[1] >> i) & 1) == 0)
    solver.add(((v[5] >> i) & 1) == 0)   
    solver.add(((v[23] >> i) & 1) == 0) 
    solver.add(((v[19] >> i) & 1) == 0)

for i in range(1,6):
    solver.add(((v[1] >> i) & 1) == 0)
    solver.add(((v[5] >> i) & 1) == 0)

for i in range(2,5):
    solver.add(((v[i] >> 23) & 1) == 0)
    solver.add(((v[i] >> 19) & 1) == 0)
    solver.add(((v[i] >> 1) & 1) == 0)
    solver.add(((v[i] >> 5) & 1) == 0)

for i in range(20,23):
    solver.add(((v[i] >> 23) & 1) == 0)
    solver.add(((v[i] >> 19) & 1) == 0)
    


# for i in range(17,20):
#     solver.add(((v[18] >> 4) & 1) == 0)
#     solver.add(((v[18] >> 8) & 1) == 0)
    
solver.add(((v[18] >> 5) & 1) == 0)
solver.add(((v[18] >> 7) & 1) == 0)
solver.add(((v[18] >> 6) & 1) == 1)

solver.add(((v[19] >> 5) & 1) == 0)
solver.add(((v[19] >> 7) & 1) == 0)
solver.add(((v[19] >> 6) & 1) == 0)

solver.add(((v[17] >> 5) & 1) == 0)
solver.add(((v[17] >> 7) & 1) == 0)
solver.add(((v[17] >> 6) & 1) == 0)
    
    
if solver.check() == sat:
    model = solver.model()
    solution = [(model[v[i]].as_long() & 0x1ffffff) for i in range(25)]
    print("Solution:", solution)
else:
    print("No solution found.")


- Though they are all 32 bit number, we just care most about their first 25 bit.
- Generating a QR code to get our flag!