tools-only Constraint Solving with Z3
Comprehensive guide to using Z3 theorem prover for symbolic execution.
Table of Contents
Z3 Basics
Installation
pip install z3-solver
Basic Workflow
from z3 import *
# 1. Create variables
x = Int('x')
y = Int('y')
# 2. Create solver
solver = Solver()
# 3. Add constraints
solver.add(x > 0)
solver.add(y < 10)
solver.add(x + y == 15)
# 4. Check satisfiability
if solver.check() == sat:
model = solver.model()
print(f"x = {model[x]}")
print(f"y = {model[y]}")
else:
print("Unsatisfiable")
Variable Types
Integer Variables
x = Int('x')
y = Int('y')
solver = Solver()
solver.add(x + y == 10)
solver.add(x > y)
if solver.check() == sat:
m = solver.model()
print(f"x={m[x]}, y={m[y]}") # e.g., x=6, y=4
Real (Floating Point) Variables
price = Real('price')
discount = Real('discount')
solver = Solver()
solver.add(price > 0)
solver.add(discount >= 0)
solver.add(discount <= price)
solver.add(price - discount == 50)
if solver.check() == sat:
m = solver.model()
print(f"price={m[price]}, discount={m[discount]}")
Boolean Variables
is_premium = Bool('is_premium')
has_coupon = Bool('has_coupon')
solver = Solver()
solver.add(Or(is_premium, has_coupon)) # At least one true
solver.add(Not(And(is_premium, has_coupon))) # Not both
if solver.check() == sat:
m = solver.model()
print(f"is_premium={m[is_premium]}, has_coupon={m[has_coupon]}")
String Variables
username = String('username')
password = String('password')
solver = Solver()
solver.add(Length(username) >= 3)
solver.add(Length(password) >= 8)
solver.add(Contains(password, StringVal("@")))
if solver.check() == sat:
m = solver.model()
print(f"username={m[username]}, password={m[password]}")
Array Variables
arr = Array('arr', IntSort(), IntSort()) # int[] in Java
i = Int('i')
solver = Solver()
solver.add(arr[0] == 5)
solver.add(arr[1] == 10)
solver.add(Select(arr, i) == 10) # arr[i] == 10
if solver.check() == sat:
m = solver.model()
print(f"i={m[i]}") # i=1
Constraint Patterns
Range Constraints
x = Int('x')
# Bounded range
solver.add(x >= 0)
solver.add(x <= 100)
# Or more concisely
solver.add(And(x >= 0, x <= 100))
Conditional Constraints
x = Int('x')
y = Int('y')
result = Int('result')
# If-then-else
solver.add(result == If(x > 0, y + 10, y - 10))
# Equivalent to:
# if x > 0:
# result = y + 10
# else:
# result = y - 10
Multiple Paths
x = Int('x')
output = Int('output')
# Path 1: x < 0
solver1 = Solver()
solver1.add(x < 0)
solver1.add(output == -x)
# Path 2: x >= 0
solver2 = Solver()
solver2.add(x >= 0)
solver2.add(output == x)
Disjunctions (OR)
x = Int('x')
# x is either negative or greater than 100
solver.add(Or(x < 0, x > 100))
# x is 5, 10, or 15
solver.add(Or(x == 5, x == 10, x == 15))
Negations
x = Int('x')
# x is NOT between 10 and 20
solver.add(Not(And(x >= 10, x <= 20)))
# Equivalent to: x < 10 OR x > 20
Solving Techniques
Basic Solving
solver = Solver()
solver.add(x > 0)
solver.add(x < 10)
result = solver.check()
if result == sat:
print("Satisfiable")
model = solver.model()
print(model)
elif result == unsat:
print("Unsatisfiable")
else:
print("Unknown")
Multiple Solutions
x = Int('x')
y = Int('y')
solver = Solver()
solver.add(x + y == 10)
solver.add(x > 0)
solver.add(y > 0)
solutions = []
for _ in range(5): # Find 5 solutions
if solver.check() == sat:
m = solver.model()
x_val = m[x].as_long()
y_val = m[y].as_long()
solutions.append((x_val, y_val))
# Block this solution
solver.add(Or(x != x_val, y != y_val))
else:
break
print(solutions) # [(1,9), (2,8), (3,7), (4,6), (5,5)]
Incremental Solving
solver = Solver()
# Add permanent constraints
solver.add(x > 0)
solver.add(y > 0)
# Try different additional constraints
solver.push() # Save state
solver.add(x + y == 10)
if solver.check() == sat:
print(solver.model())
solver.pop() # Restore state
solver.push()
solver.add(x + y == 20)
if solver.check() == sat:
print(solver.model())
solver.pop()
Unsatisfiable Core
Find minimal set of constraints that cause unsatisfiability.
x = Int('x')
c1 = x > 10
c2 = x < 5
c3 = x >= 0
solver = Solver()
solver.add(c1)
solver.add(c2)
solver.add(c3)
if solver.check() == unsat:
core = solver.unsat_core()
print(f"Unsatisfiable core: {core}")
Advanced Features
Quantifiers
x = Int('x')
# Universal quantification: ∀x. x > 0 → x^2 > 0
solver.add(ForAll([x], Implies(x > 0, x*x > 0)))
# Existential quantification: ∃x. x > 0 ∧ x < 10
solver.add(Exists([x], And(x > 0, x < 10)))
Optimization
Find maximum/minimum values.
from z3 import Optimize
x = Int('x')
y = Int('y')
opt = Optimize()
opt.add(x + y <= 10)
opt.add(x >= 0)
opt.add(y >= 0)
# Maximize x + y
opt.maximize(x + y)
if opt.check() == sat:
m = opt.model()
print(f"Optimal: x={m[x]}, y={m[y]}")
Theories
Bit-Vectors:
x = BitVec('x', 32) # 32-bit integer
y = BitVec('y', 32)
solver = Solver()
solver.add(x + y == 0xFFFFFFFF) # Check for overflow
Arrays:
arr = Array('arr', IntSort(), IntSort())
i = Int('i')
j = Int('j')
solver.add(arr[i] > arr[j])
solver.add(i < j)
solver.add(i >= 0)
solver.add(j < 10)
Complete Examples
Example 1: Finding Division by Zero
from z3 import *
def find_division_by_zero():
"""Find inputs that cause division by zero."""
a = Int('a')
b = Int('b')
c = Int('c')
# Code: result = a / (b - c)
solver = Solver()
# Error condition: denominator is zero
solver.add(b - c == 0)
# Additional constraints
solver.add(a > 0)
solver.add(b >= 0)
solver.add(c >= 0)
if solver.check() == sat:
m = solver.model()
print("ERROR: Division by zero possible!")
print(f" a={m[a]}, b={m[b]}, c={m[c]}")
return True
else:
print("Safe: No division by zero")
return False
find_division_by_zero()
# Output: ERROR: Division by zero possible!
# a=1, b=5, c=5
Example 2: Buffer Overflow Detection
from z3 import *
def find_buffer_overflow():
"""Find array index that causes overflow."""
arr_size = 10
index = Int('index')
value = Int('value')
solver = Solver()
# Error condition: index out of bounds
solver.add(Or(index < 0, index >= arr_size))
# Additional constraints from code
solver.add(value > 0)
solver.add(index == value - 1)
if solver.check() == sat:
m = solver.model()
print("ERROR: Buffer overflow possible!")
print(f" index={m[index]}, value={m[value]}")
return True
else:
print("Safe: No buffer overflow")
return False
find_buffer_overflow()
Example 3: Path Constraint Solving
from z3 import *
def solve_path_constraints():
"""Solve constraints for all paths through code."""
# Code:
# if x > 0:
# if y > 10:
# result = x + y
# else:
# result = x - y
# else:
# result = 0
x = Int('x')
y = Int('y')
result = Int('result')
paths = [
("Path 1: x>0, y>10", [x > 0, y > 10, result == x + y]),
("Path 2: x>0, y<=10", [x > 0, y <= 10, result == x - y]),
("Path 3: x<=0", [x <= 0, result == 0])
]
for path_name, constraints in paths:
solver = Solver()
solver.add(constraints)
if solver.check() == sat:
m = solver.model()
print(f"{path_name}")
print(f" x={m[x]}, y={m[y]}, result={m[result]}")
else:
print(f"{path_name}: Infeasible")
solve_path_constraints()
Example 4: String Constraints
from z3 import *
def validate_input():
"""Find inputs that satisfy validation rules."""
username = String('username')
password = String('password')
solver = Solver()
# Validation rules
solver.add(Length(username) >= 3)
solver.add(Length(username) <= 20)
solver.add(Length(password) >= 8)
solver.add(Contains(password, StringVal("@")))
solver.add(Contains(password, StringVal("1")))
if solver.check() == sat:
m = solver.model()
print("Valid input found:")
print(f" username={m[username]}")
print(f" password={m[password]}")
validate_input()
Tips
- Start simple: Begin with basic constraints, add complexity gradually
- Use appropriate types: Int for integers, Real for floats, String for text
- Check satisfiability: Always check if solver.check() == sat before accessing model
- Add bounds: Constrain variables to reasonable ranges to speed up solving
- Incremental solving: Use push/pop for trying different constraint sets
- Multiple solutions: Block previous solutions to find alternatives
- Debugging: Print constraints with
print(solver)to see what you're solving - Performance: Simpler constraints solve faster; avoid unnecessary quantifiers
Common Patterns
Pattern: Explore All Branches
def explore_branches(conditions):
"""Generate test inputs for all branch combinations."""
for i, condition_set in enumerate(conditions):
solver = Solver()
solver.add(condition_set)
if solver.check() == sat:
print(f"Branch {i}: {solver.model()}")
Pattern: Find Error Inputs
def find_error(error_condition, context_constraints):
"""Find inputs that trigger an error."""
solver = Solver()
solver.add(error_condition)
solver.add(context_constraints)
if solver.check() == sat:
return solver.model()
return None
Pattern: Verify Safety
def verify_safe(safety_property, all_paths):
"""Verify safety property holds on all paths."""
for path_constraints in all_paths:
solver = Solver()
solver.add(path_constraints)
solver.add(Not(safety_property)) # Negate property
if solver.check() == sat:
print(f"VIOLATION: {solver.model()}")
return False
print("SAFE: Property holds on all paths")
return True