Z3 Solver Quick Reference
=========================

INSTALLATION
  pip install z3-solver

BASIC USAGE
  from z3 import *

  # Create solver
  s = Solver()

  # Declare variables
  x = Int('x')              Integer variable
  y = Int('y')
  a = BitVec('a', 32)       32-bit bitvector
  b = BitVec('b', 32)
  r = Real('r')             Real number
  flag = [BitVec(f'f{i}', 8) for i in range(20)]  # Array

CONSTRAINTS
  s.add(x + y == 10)        Add constraint
  s.add(x > 0)              Inequality
  s.add(x != y)             Not equal
  s.add(And(x > 0, y > 0))  Logical AND
  s.add(Or(x == 1, x == 2)) Logical OR
  s.add(Not(x == 0))        Logical NOT
  s.add(If(x > 0, y, z) == 5) Conditional

SOLVING
  if s.check() == sat:
      m = s.model()
      print(m[x])            Get value
      print(m.eval(x + y))   Evaluate expression
  else:
      print("No solution")

BITVECTOR OPERATIONS
  a + b                 Addition
  a - b                 Subtraction
  a * b                 Multiplication
  a & b                 Bitwise AND
  a | b                 Bitwise OR
  a ^ b                 Bitwise XOR
  ~a                    Bitwise NOT
  a << 2                Left shift
  LShR(a, 2)            Logical right shift
  a >> 2                Arithmetic right shift
  RotateLeft(a, n)      Rotate left
  RotateRight(a, n)     Rotate right
  ZeroExt(n, a)         Zero extend
  SignExt(n, a)         Sign extend
  Extract(hi, lo, a)    Extract bits [hi:lo]
  Concat(a, b)          Concatenate bitvectors

COMMON CTF PATTERNS
  # Solve for flag bytes (printable ASCII)
  flag = [BitVec(f'f{i}', 8) for i in range(N)]
  s = Solver()
  for f in flag:
      s.add(f >= 0x20, f <= 0x7e)

  # Add challenge-specific constraints
  s.add(flag[0] == ord('i'))  # icoa{...}

  if s.check() == sat:
      m = s.model()
      result = ''.join(chr(m[f].as_long()) for f in flag)
      print(result)

  # Reverse a hash-like function
  def transform(x):
      return (x * 1337 + 42) & 0xFFFFFFFF

  target = 0xDEADBEEF
  x = BitVec('x', 32)
  s = Solver()
  s.add(transform(x) == target)
