Z3 SMT Solver Practice Hub

Challenge 1: sub_140001010

Easy Basic Linear Math

__int64 __fastcall verify_key(unsigned int a1, unsigned int a2)
{
  if ( (3 * a1 + 2 * a2 != 180) )
    return 0LL;
  if ( (a1 - a2 != 10) )
    return 0LL;
  return 1LL;
}

Skills: Systems of linear equations. Model `a1` and `a2` as Z3 integers.

Concept — SMT Solving & Systems of Equations: SMT (Satisfiability Modulo Theories) solvers decide if logical/arithmetic formulas are satisfiable. Instead of solving equations by hand (using substitution or elimination), you declare variables and add constraints. Z3 automatically resolves them.

Candidate Options

STATUS: NOT_SOLVED

Hint

Use `a1, a2 = Ints('a1 a2')` in Python Z3, add the two equations, and output the model results.

Python Z3 Solver Script

from z3 import *

a1, a2 = Ints('a1 a2')
s = Solver()
s.add(3 * a1 + 2 * a2 == 180)
s.add(a1 - a2 == 10)

if s.check() == sat:
    print(s.model())

Challenge 2: sub_1400011C0

Easy Quadratic bounds

bool __fastcall validate_serial(int input_val)
{
  int calculated; // [rsp+18h] [rbp-4h]

  calculated = input_val * input_val - 40 * input_val;
  return input_val > 0 && calculated == 1200;
}

Skills: Quadratic equations and inequalities in Z3.

Concept — Nonlinear Constraints & Quadratic Bounds: Reversing polynomial expressions (like quadratic equations \(x^2 - 40x = 1200\)) manually requires factoring or the quadratic formula. SMT solvers handle these nonlinear equations and range bounds (e.g. \(x > 0\)) by representing them as mathematical intervals and searching for valid integers.

Candidate Options

STATUS: NOT_SOLVED

Hint

Define a single variable `x = Int('x')`. Add constraints `x > 0` and `x * x - 40 * x == 1200`.

Python Z3 Solver Script

from z3 import *

x = Int('x')
s = Solver()
s.add(x > 0)
s.add(x * x - 40 * x == 1200)

if s.check() == sat:
    print(s.model())

Challenge 3: sub_1400012A0

Easy Signed 8-bit Overflow

__int64 __fastcall check_byte(__int8 key)
{
  __int8 temporary; 

  temporary = 7 * key + 12;
  return temporary == -46; // Watch out for signed 8-bit wrap around!
}

Skills: Modeling overflow using Bit-Vectors in Z3. Return the unsigned value (0-255).

Concept — Bit-Vector Arithmetic & Signed Overflow: CPU registers have a fixed width (like 8-bit `__int8`). Arithmetic overflows (e.g., \(127 + 1 = -128\)) and sign extensions are common in compiled code. Z3's `BitVec` types simulate this exact machine-level overflow behavior, whereas mathematical `Int` types do not wrap around.

Candidate Options

STATUS: NOT_SOLVED

Hint

Model `key` as an 8-bit Bit-Vector: `key = BitVec('key', 8)`. Use equation `7 * key + 12 == -46`. Retrieve the integer output in Python.

Python Z3 Solver Script

from z3 import *

key = BitVec('key', 8)
s = Solver()
s.add(7 * key + 12 == -46)

if s.check() == sat:
    print(s.model()[key].as_long())

Challenge 4: sub_140001350

Easy String Character math

bool __fastcall verify_str(char *str)
{
  if ( str[0] != 'c' )
    return false;
  if ( str[1] + str[0] != 210 )
    return false;
  if ( (str[2] ^ str[1]) != 13 )
    return false;
  return str[3] == 0;
}

Skills: Character calculations. Solve for a 3-character string.

Concept — ASCII Boundary Constraints: When reversing string validations, bytes represent ASCII characters. To restrict Z3 from giving unprintable or negative solutions, you must constrain the variables to the printable ASCII range (\(32 \le \text{char} \le 126\)) to ensure a valid text output.

Candidate Options

STATUS: NOT_SOLVED

Hint

Model indices `str[0]`, `str[1]`, `str[2]` as 8-bit bitvectors or integers. Convert solved values back to ASCII characters.

Python Z3 Solver Script

from z3 import *

chars = [BitVec(f'c_{i}', 8) for i in range(3)]
s = Solver()
s.add(chars[0] == ord('c'))
s.add(chars[1] + chars[0] == 210)
s.add(chars[2] ^ chars[1] == 13)

if s.check() == sat:
    m = s.model()
    print("".join(chr(m[c].as_long()) for c in chars))

Challenge 5: sub_1400015F0

Easy Bitwise Masking

__int64 __fastcall bit_kernel(unsigned __int16 input)
{
  if ( (input & 0xFF00) != 0xDE00 )
    return 0LL;
  if ( (input ^ 0x00FF) != 0xDEAD )
    return 0LL;
  return 1LL;
}

Skills: 16-bit Bit-Vector constraints (AND, XOR).

Concept — Bitwise Masking (AND/XOR): Decompilers use bitwise `&` (AND) to mask off specific byte sections, and `^` (XOR) for basic encryption. SMT solvers analyze these bitwise relations at the individual bit level by "bit-blasting" the constraints into boolean SAT gates.

Candidate Options

STATUS: NOT_SOLVED

Hint

Create `input = BitVec('input', 16)`. Add the two constraints and solve. Output the base-10 representation.

Python Z3 Solver Script

from z3 import *

input_val = BitVec('input_val', 16)
s = Solver()
s.add(input_val & 0xFF00 == 0xDE00)
s.add(input_val ^ 0x00FF == 0xDEAD)

if s.check() == sat:
    print(s.model()[input_val].as_long())

Challenge 6: sub_140001700

Easy Array index relation

bool __fastcall array_checker(unsigned int *arr)
{
  // arr contains 3 elements
  if ( arr[0] + arr[1] != 100 ) return false;
  if ( arr[1] * arr[2] != 1200 ) return false;
  if ( arr[2] - arr[0] != 10 ) return false;
  return true;
}

Skills: Modeling arrays of integers. Format: `x,y,z` for `arr[0],arr[1],arr[2]`.

Concept — Array Modeling: In decompiler output, static buffers or arrays are often indexed directly. SMT solvers can model arrays by declaring individual variables for each offset or using Z3's formal `Array` type to represent memory reads and writes.

Candidate Options

STATUS: NOT_SOLVED

Hint

Model three Z3 variables: `x, y, z = Ints('x y z')`. Solve and input as comma-separated integers.

Python Z3 Solver Script

from z3 import *

arr = [Int(f'arr_{i}') for i in range(3)]
s = Solver()
s.add(arr[0] + arr[1] == 100)
s.add(arr[1] * arr[2] == 1200)
s.add(arr[2] - arr[0] == 10)

if s.check() == sat:
    print(s.model())

Challenge 7: sub_140001850

Easy Modulo constraints

__int64 __fastcall modulo_lock(int secret)
{
  if ( secret <= 1000 )
    return 0LL;
  if ( secret % 11 != 5 )
    return 0LL;
  if ( secret % 13 != 3 )
    return 0LL;
  return secret < 1150;
}

Skills: Multi-modulo boundary constraints.

Concept — Modulo Constraints & Diophantine Equations: The modulo operator `%` creates cyclical groups. Equations involving modular residues are called Diophantine equations. Z3 uses advanced congruence heuristics to find integer solutions satisfying multiple modulo constraints simultaneously.

Candidate Options

STATUS: NOT_SOLVED

Hint

Create `secret = Int('secret')`. Add constraints: `secret > 1000`, `secret < 1150`, `secret % 11 == 5`, `secret % 13 == 3`.

Python Z3 Solver Script

from z3 import *

secret = Int('secret')
s = Solver()
s.add(secret > 1000)
s.add(secret < 1150)
s.add(secret % 11 == 5)
s.add(secret % 13 == 3)

if s.check() == sat:
    print(s.model())

Challenge 8: sub_1400019C0

Easy Bit Shifting

bool __fastcall shift_check(unsigned int flag)
{
  unsigned int v1;
  unsigned int v2;

  v1 = flag >> 4;
  v2 = flag << 3;
  return (v1 == 0x123) && ((v2 & 0xFF) == 0x28);
}

Skills: Left and right shift simulation in Z3 Bit-Vectors.

Concept — Bit Shifting (Logical vs. Arithmetic): Bit shifts (`<<`, `>>`) translate bits left or right, introducing zeros or propagating sign bits. Since shifting discards bits, Z3 models shifts as bitvector operations to resolve the original values based on the remaining bits.

Candidate Options

STATUS: NOT_SOLVED

Hint

Model `flag` as a 32-bit Bit-Vector: `flag = BitVec('flag', 32)`. Add constraints using Z3 shift operators `>>` and `<<`.

Python Z3 Solver Script

from z3 import *

flag = BitVec('flag', 32)
s = Solver()
v1 = flag >> 4;
v2 = flag << 3;
s.add(v1 == 0x123)
s.add((v2 & 0xFF) == 0x28)

if s.check() == sat:
    print(s.model()[flag].as_long())

Challenge 9: sub_140001AF0

Easy Multi-variable linear equations

__int64 __fastcall multi_check(int x, int y, int z)
{
  if ( 5 * x - 3 * y + 2 * z != 29 )
    return 0LL;
  if ( 2 * x + 4 * y - 5 * z != 5 )
    return 0LL;
  if ( 3 * x - 2 * y + 4 * z != 34 )
    return 0LL;
  return 1LL;
}

Skills: 3-variable system of linear equations. Format: `x,y,z`.

Concept — High-Dimensional Linear Systems: Reversing systems of equations with three or more variables is tedious. Z3 handles high-dimensional systems by applying matrix-like Gaussian elimination and simplex algorithms internally.

Candidate Options

STATUS: NOT_SOLVED

Hint

Define `x, y, z = Ints('x y z')`. Add the 3 linear checks, check status, and retrieve values.

Python Z3 Solver Script

from z3 import *

x, y, z = Ints('x y z')
s = Solver()
s.add(5 * x - 3 * y + 2 * z == 29)
s.add(2 * x + 4 * y - 5 * z == 5)
s.add(3 * x - 2 * y + 4 * z == 34)

if s.check() == sat:
    print(s.model())

Challenge 10: sub_140001C50

Easy Murmur-ish transform

bool __fastcall final_boss(unsigned int key)
{
  unsigned int transform;

  transform = key ^ 0x55555555;
  transform = (transform >> 16) | (transform << 16); // 16-bit block rotate
  transform += 0x1337;
  return transform == 0xDEADBEEF;
}

Skills: Mixed bitwise rotations, XOR, and arithmetic additions.

Concept — Circular Bit Rotations: Decompilers optimize rotations (ROL/ROR) using shift combinations: `(x >> 16) | (x << 16)`. These operations swap byte blocks, and are modeled in Z3 using bitwise ORs on shifted bitvectors.

Candidate Options

STATUS: NOT_SOLVED

Hint

Create `key = BitVec('key', 32)`. Replicate the rotate operation using `((transform >> 16) | (transform << 16))` inside Z3. Beware of shift boundaries in 32-bit.

Python Z3 Solver Script

from z3 import *

key = BitVec('key', 32)
s = Solver()
transform = key ^ 0x55555555
transform = RotateRight(transform, 16)
s.add(transform + 0x1337 == 0xDEADBEEF)

if s.check() == sat:
    print(s.model()[key].as_long())

Challenge 11: sub_140002100

Medium Matrix Modulo 256

bool __fastcall check_matrix(unsigned char *a)
{
  if ( (5*a[0] + 3*a[1] + 8*a[2] + 2*a[3]) % 256 != 189 ) return false;
  if ( (2*a[0] + 9*a[1] +   a[2] + 4*a[3]) % 256 != 23 )  return false;
  if ( (  a[0] + 4*a[1] + 7*a[2] + 5*a[3]) % 256 != 107 ) return false;
  if ( (8*a[0] + 6*a[1] + 3*a[2] + 9*a[3]) % 256 != 148 ) return false;
  return true;
}

Skills: Linear systems over modular algebra. Model bytes using `BitVec(..., 8)` or `Int` with modulo constraints. Format: `a[0],a[1],a[2],a[3]`.

Concept — Matrix Systems over Finite Rings: In cryptography, linear diffusion steps are often represented as matrix multiplications modulo a power of two (typically modulo 256 for bytes). Z3 models these modulo-ring matrices without needing matrix inversion.

Candidate Options

STATUS: NOT_SOLVED

Hint

Define 4 variables as `BitVecs('a b c d', 8)`. Set up equations using `+` and `*` operators. Note: the third equation is `4*a + b + 7*c + 5*d == 107` (IDA decompiler optimization details: `4 * a[0] + a[1]` is optimized as `a[1] + 4 * a[0]`).

Python Z3 Solver Script

from z3 import *

a = [BitVec(f'a_{i}', 8) for i in range(4)]
s = Solver()
s.add((5*a[0] + 3*a[1] + 8*a[2] + 2*a[3]) == 189)
s.add((2*a[0] + 9*a[1] + a[2] + 4*a[3]) == 23)
s.add((4*a[0] + a[1] + 7*a[2] + 5*a[3]) == 107)
s.add((8*a[0] + 6*a[1] + 3*a[2] + 9*a[3]) == 148)

if s.check() == sat:
    print(s.model())

Challenge 12: sub_140002200

Medium Mixed Addition & XOR

bool __fastcall validate_keys(unsigned int x, unsigned int y)
{
  unsigned int combined_xor = x ^ y;
  unsigned int combined_sum = x + y;

  return (combined_xor == 0x5599B9F9) 
      && (combined_sum == 0x9999BE01) 
      && ((x & 0xFFFF0000) == 0x32100000);
}

Skills: Reversing mixed arithmetic (addition) and bitwise (XOR) operators. Hand analysis is highly difficult due to carry propagation. Format: `x,y`.

Concept — Mixed Boolean-Arithmetic (MBA): Code that mixes arithmetic addition (`+`) with bitwise operations (`^`, `&`) is called MBA. Reversing MBA expressions by hand is extremely difficult because carries propagate unpredictably. Z3 solves this easily by analyzing carry chains in bit-vector representation.

Candidate Options

STATUS: NOT_SOLVED

Hint

Model `x` and `y` as 32-bit Bit-Vectors (`BitVec('x', 32)`). Add the three constraints. The carry bits will be solved automatically by Z3's bit-blasting engine.

Python Z3 Solver Script

from z3 import *

x, y = BitVecs('x y', 32)
s = Solver()
s.add(x ^ y == 0x5599B9F9)
s.add(x + y == 0x9999BE01)
s.add(x & 0xFFFF0000 == 0x32100000)

if s.check() == sat:
    print(s.model())

Challenge 13: sub_140002300

Medium djb2 Hash Collision

bool __fastcall verify_hash(const char *str)
{
  unsigned int hash = 5381;
  int i;

  for ( i = 0; i < 6; ++i )
  {
    if ( str[i] < 32 || str[i] > 126 ) return false;
    hash = 33 * hash + str[i];
  }
  return hash == 0x284FC66A;
}

Skills: Loop modeling, hash preimages, character boundaries. Find a 6-character printable string. (Multiple inputs may collide and be valid!)

Concept — Loop Unrolling & Hash Collisions: SMT solvers evaluate loops by unrolling them into a static chain of constraints. This allows Z3 to search for "preimages" (input values) that yield a specific target hash, which is useful for finding hash collisions.

Candidate Options

STATUS: NOT_SOLVED

Hint

Use Z3 `Int` for each of the 6 characters to prevent slow bitvector division. Model the hash step as: `hash = (hash * 33 + chars[i]) % 4294967296`. Add bounds `chars[i] >= 32` and `chars[i] <= 126`. One solution is `'z3rule'`.

Python Z3 Solver Script

from z3 import *

chars = [Int(f'c_{i}') for i in range(6)]
s = Solver()
for c in chars:
    s.add(c >= 32, c <= 126)

h = 5381
for c in chars:
    h = (h * 33 + c) % 4294967296

s.add(h == 0x284FC66A)

if s.check() == sat:
    m = s.model()
    print("".join(chr(m[c].as_long()) for c in chars))

Challenge 14: sub_140002400

Medium Non-linear Modulo

bool __fastcall check_nonlinear(unsigned __int16 a, unsigned __int16 b, unsigned __int16 c)
{
  if ( a <= 1000 || b <= 1000 || c <= 1000 ) return false;
  
  if ( (a * b + c) % 65536 != 3312 )   return false;
  if ( (b * c + a) % 65536 != 53290 )  return false;
  if ( ((a ^ b) << 4) % 65536 != 0x2FC0 ) return false;
  return true;
}

Skills: Non-linear multiplication mixed with bitwise XOR on 16-bit ranges. Format: `a,b,c`.

Concept — Non-Linear Modular Multiplication: Equations containing products of symbolic variables under a modulo ring (e.g., `(a * b) % 65536`) are highly non-linear and NP-hard to reverse. Z3 resolves these by using specialized SMT solvers for bit-vectors.

Candidate Options

STATUS: NOT_SOLVED

Hint

Model variables as 16-bit Bit-Vectors (`BitVec('a', 16)`). Let multiplication wrap around naturally as it does in 16-bit arithmetic. Z3 can solve non-linear multiplication over finite fields very quickly.

Python Z3 Solver Script

from z3 import *

a, b, c = BitVecs('a b c', 16)
s = Solver()
s.add(a > 1000, b > 1000, c > 1000)
s.add(a * b + c == 3312)
s.add(b * c + a == 53290)
s.add(((a ^ b) << 4) == 0x2FC0)

if s.check() == sat:
    print(s.model())

Challenge 15: sub_140002500

Medium Array Permutation & Sum

bool __fastcall verify_array(unsigned int *arr)
{
  unsigned int temp[4];
  
  temp[0] = arr[2] + 15;
  temp[1] = arr[0] ^ arr[3];
  temp[2] = arr[1] * 3;
  temp[3] = arr[3] - arr[2];

  return (temp[0] == 100) 
      && (temp[1] == 1337) 
      && (temp[2] == 999) 
      && (temp[3] == 500)
      && (arr[0] + arr[1] + arr[2] + arr[3] == 2843);
}

Skills: Tracking shuffled variables and multi-variable dependencies. Format: `arr[0],arr[1],arr[2],arr[3]`.

Concept — Variable Permutation & Shuffling: Algorithms often shuffle elements in temporary buffers. Modeling these requires keeping track of the intermediate variables as they are swapped and assigned.

Candidate Options

STATUS: NOT_SOLVED

Hint

Create 4 variables `arr = [BitVec(f'a_{i}', 32) for i in range(4)]`. Set up the temporary variables exactly as shown, add the constraints, and output the results.

Python Z3 Solver Script

from z3 import *

arr = [BitVec(f'arr_{i}', 32) for i in range(4)]
s = Solver()

temp0 = arr[2] + 15
temp1 = arr[0] ^ arr[3]
temp2 = arr[1] * 3
temp3 = arr[3] - arr[2]

s.add(temp0 == 100)
s.add(temp1 == 1337)
s.add(temp2 == 999)
s.add(temp3 == 500)
s.add(arr[0] + arr[1] + arr[2] + arr[3] == 2843)

if s.check() == sat:
    print(s.model())

Challenge 16: sub_140003100

Hard VM Register Mixer

bool __fastcall mix_registers(unsigned int k1, unsigned int k2, unsigned int k3)
{
  unsigned int r0 = k1;
  unsigned int r1 = k2;
  unsigned int r2 = k3;

  r0 = (r0 ^ r1) + r2;
  r1 = (r1 + r2) ^ r0;
  r2 = (r2 ^ r0) + r1;

  r0 = (r0 << 5) | (r0 >> 27); // ROL 5
  r1 = (r1 >> 3) | (r1 << 29); // ROR 3
  r2 ^= 0x90ABCDEF;

  return (r0 == 0x12345678) 
      && (r1 == 0x87654321) 
      && (r2 == 0xABCDEF01);
}

Skills: Modeling state transitions, bitwise rotations, and mixed addition/XOR diffusion. Format: `k1,k2,k3`.

Concept — VM Register Files & State Transitions: Custom virtual machine interpreters use a set of registers (like `R0`, `R1`, `R2`) that are updated at each instruction. To solve VM constraints, you model the register array's state transitions chronologically.

Candidate Options

STATUS: NOT_SOLVED

Hint

Use 32-bit Bit-Vectors. Replicate rotations using `RotateLeft(r0, 5)` and `RotateRight(r1, 3)` from the `z3` Python library. Add the final equality checks and output the base-10 values.

Python Z3 Solver Script

from z3 import *

k1, k2, k3 = BitVecs('k1 k2 k3', 32)
s = Solver()

r0 = (k1 ^ k2) + k3
r1 = (k2 + k3) ^ r0
r2 = (k3 ^ r0) + r1

r0 = RotateLeft(r0, 5)
r1 = RotateRight(r1, 3)
r2 ^= 0x90ABCDEF

s.add(r0 == 0x12345678)
s.add(r1 == 0x87654321)
s.add(r2 == 0xABCDEF01)

if s.check() == sat:
    print(s.model())

Challenge 17: sub_140003200

Hard S-Box substitution & Diffusion

bool __fastcall sbox_layer(unsigned char *key)
{
  const unsigned char sbox[16] = { 
    0xC, 0x5, 0x6, 0xB, 0x9, 0x0, 0xA, 0xD, 
    0x3, 0xE, 0xF, 0x8, 0x4, 0x7, 0x1, 0x2 
  };
  unsigned char a, b, c, d;

  a = (sbox[key[0] >> 4] << 4) | sbox[key[0] & 0xF];
  b = (sbox[key[1] >> 4] << 4) | sbox[key[1] & 0xF];
  c = (sbox[key[2] >> 4] << 4) | sbox[key[2] & 0xF];
  d = (sbox[key[3] >> 4] << 4) | sbox[key[3] & 0xF];

  return (a ^ b ^ c == 0xAA) 
      && (b ^ c ^ d == 0xBB) 
      && (c ^ d ^ a == 0xCC) 
      && (d ^ a ^ b == 0xDD);
}

Skills: Modeling lookup tables and substitution layers in Z3. Format: `key[0],key[1],key[2],key[3]`.

Concept — Lookup Tables (S-Boxes): Cryptography utilizes non-linear lookup tables (S-Boxes) for confusion. Since array lookups with symbolic indices are complex, they are modeled in Z3 using nested conditional expressions (`If(val == i, sbox[i], ...)`) to represent every possible mapping.

Candidate Options

STATUS: NOT_SOLVED

Hint

Model lookup using Z3 nested `If` constraints. For a 4-bit value `val`, do `res = If(val == 0, 12, If(val == 1, 5, ...))`. Perform this lookup on both high and low nibbles of each key byte, then enforce the diffusion XOR equations.

Python Z3 Solver Script

from z3 import *

key = [BitVec(f'key_{i}', 8) for i in range(4)]
s = Solver()

sbox_vals = [0xC, 0x5, 0x6, 0xB, 0x9, 0x0, 0xA, 0xD, 0x3, 0xE, 0xF, 0x8, 0x4, 0x7, 0x1, 0x2]

def sbox_lookup(val):
    res = BitVecVal(0, 4)
    for i in range(16):
        res = If(val == i, BitVecVal(sbox_vals[i], 4), res)
    return res

def sbox_byte(b):
    return Concat(sbox_lookup((b >> 4) & 0xF), sbox_lookup(b & 0xF))

a = sbox_byte(key[0])
b = sbox_byte(key[1])
c = sbox_byte(key[2])
d = sbox_byte(key[3])

s.add(a ^ b ^ c == 0xAA)
s.add(b ^ c ^ d == 0xBB)
s.add(c ^ d ^ a == 0xCC)
s.add(d ^ a ^ b == 0xDD)

if s.check() == sat:
    print(s.model())

Challenge 18: sub_140003300

Hard Custom LFSR

bool __fastcall lfsr_check(unsigned int seed)
{
  unsigned int state = seed;
  unsigned int bit;
  int i;

  for ( i = 0; i < 16; ++i )
  {
    bit = (state ^ (state >> 2) ^ (state >> 3) ^ (state >> 5)) & 1;
    state = (state >> 1) | (bit << 31);
  }
  return state == 0x1B7E1337;
}

Skills: Modeling loops and bit-level feedback structures. Hand-reversing is highly tedious due to shifting overlaps.

Concept — LFSR & Loop Variable Chaining: A Linear Feedback Shift Register (LFSR) shifts bits recursively based on XOR feedback taps. To prevent exponential growth of symbolic expressions across clock cycles, you define a new Z3 variable for each step.

Candidate Options

STATUS: NOT_SOLVED

Hint

Define an array of 17 variables `states = [BitVec(f'state_{i}', 32) for i in range(17)]` to prevent exponential growth in symbolic expressions. Enforce `states[i+1] == (states[i] >> 1) | (ZeroExt(31, bit) << 31)` with the appropriate XOR taps extracted using `Extract(bit_pos, bit_pos, states[i])`.

Python Z3 Solver Script

from z3 import *

seed = BitVec('seed', 32)
states = [BitVec(f'state_{i}', 32) for i in range(17)]
s = Solver()

s.add(states[0] == seed)
for i in range(16):
    bit = (Extract(0, 0, states[i]) ^ Extract(2, 2, states[i]) ^ Extract(3, 3, states[i]) ^ Extract(5, 5, states[i]))
    s.add(states[i+1] == (states[i] >> 1) | (ZeroExt(31, bit) << 31))

s.add(states[16] == 0x1B7E1337)

if s.check() == sat:
    print(s.model()[seed].as_long())

Challenge 19: sub_140003400

Hard Division & Remainder System

bool __fastcall diophantine_check(unsigned int x, unsigned int y)
{
  if ( x + y != 500000 ) return false;

  if ( (x / 1337) + (y % 999) != 301 ) return false;
  if ( (y / 1337) + (x % 999) != 572 ) return false;
  return true;
}

Skills: Modeling integer division and modulus operations. SMT solvers solve this via arithmetic domain reductions. Format: `x,y`.

Concept — Modulo-Division Constraints: Non-linear equations with mixed division and remainder (e.g., `(x / d) + (y % m)`) are difficult due to the step-like nature of integer division. Z3 mathematical `Int` is much faster than `BitVec` for pure division constraints.

Candidate Options

STATUS: NOT_SOLVED

Hint

Use mathematical integers `x, y = Ints('x y')` in Z3 rather than Bit-Vectors. Division `/` and remainder `%` on Z3 `Int` are extremely optimized compared to `BitVec` divisions, solving in milliseconds.

Python Z3 Solver Script

from z3 import *

x, y = Ints('x y')
s = Solver()
s.add(x >= 0, y >= 0)
s.add(x + y == 500000)
s.add(x / 1337 + y % 999 == 301)
s.add(y / 1337 + x % 999 == 572)

if s.check() == sat:
    print(s.model())

Challenge 20: sub_140003500

Hard Single Round TEA Decryption

bool __fastcall tea_round(unsigned int *k)
{
  unsigned int v0 = 0x01234567;
  unsigned int v1 = 0x89ABCDEF;
  unsigned int sum = 0x9E3779B9;

  v0 += ((v1 << 4) + k[0]) ^ (v1 + sum) ^ ((v1 >> 5) + k[1]);
  v1 += ((v0 << 4) + k[2]) ^ (v0 + sum) ^ ((v0 >> 5) + k[3]);

  return (v0 == 0xDEADBEEF) && (v1 == 0xCAFEBABE);
}

Skills: Decrypting cipher schedules. Solve for the 4-word key `k[0],k[1],k[2],k[3]`. Z3 handles cryptographic constraint systems cleanly.

Concept — Block Cipher Inversion: Reversing a round of a block cipher (like TEA) involves resolving mixed XOR, shift, and addition keys. Z3 decrypts this by defining the end states as constants and letting the solver compute the key inputs.

Candidate Options

STATUS: NOT_SOLVED

Hint

Define 4 variables as 32-bit Bit-Vectors. Substitute constants `v0, v1, sum` exactly as they are defined. Set the final constraints and print the values in decimal.

Python Z3 Solver Script

from z3 import *

k = [BitVec(f'k_{i}', 32) for i in range(4)]
s = Solver()

v0 = BitVecVal(0x01234567, 32)
v1 = BitVecVal(0x89ABCDEF, 32)
sum_val = BitVecVal(0x9E3779B9, 32)

v0 += ((v1 << 4) + k[0]) ^ (v1 + sum_val) ^ ((v1 >> 5) + k[1])
v1 += ((v0 << 4) + k[2]) ^ (v0 + sum_val) ^ ((v0 >> 5) + k[3])

s.add(v0 == 0xDEADBEEF)
s.add(v1 == 0xCAFEBABE)

if s.check() == sat:
    print(s.model())