Skip to main content

​
What is SMT?

Satisfiability Modulo Theories (SMT) is a decision problem for logical formulas with respect to combinations of background theories. Z3 is a state-of-the-art SMT solver that can determine whether a formula is satisfiable, unsatisfiable, or unknown.

​
Core Concepts

​
Satisfiability

A formula is satisfiable if there exists an assignment of values to variables that makes the formula true. Z3 returns one of three possible results:
  • sat - The formula is satisfiable (a model exists)
  • unsat - The formula is unsatisfiable (no solution exists)
  • unknown - Z3 could not determine satisfiability (timeout, resource limits, etc.)

​
Theories

Z3 supports multiple background theories that can be combined:

Linear Arithmetic

Integer and real linear arithmetic (LIA, LRA)

Bit-Vectors

Fixed-size bit-vector arithmetic

Arrays

Extensional array theory with select/store

Uninterpreted Functions

Functions with no specified interpretation

Datatypes

Algebraic datatypes and records

Strings

String operations and regular expressions

​
Basic SMT Solving Example

from z3 import *

# Create variables
x = Int('x')
y = Int('y')

# Create solver
s = Solver()

# Add constraints
s.add(x > 10)
s.add(y > x)
s.add(y < 15)

# Check satisfiability
result = s.check()
print(result)  # sat

if result == sat:
    m = s.model()
    print(f"x = {m[x]}, y = {m[y]}")

​
Theory Combination

Z3’s power comes from combining multiple theories. Here’s an example mixing arithmetic and arrays: 
from z3 import *

# Array theory with integer indices and values
A = Array('A', IntSort(), IntSort())
i = Int('i')
j = Int('j')

s = Solver()
# Array constraints
s.add(Store(A, i, 10)[j] == 10)  # Store 10 at index i, then read at j
s.add(i != j)                      # i and j are different

print(s.check())  # unsat - contradiction!

​
Proving Validity

To prove a formula φ is valid (true under all interpretations), check if ¬φ is unsatisfiable: 
from z3 import *

def prove(conjecture):
    s = Solver()
    s.add(Not(conjecture))
    
    if s.check() == unsat:
        print("Proved!")
    else:
        print("Counterexample:")
        print(s.model())

# Example: x = y implies f(x) = f(y)
x, y = Ints('x y')
f = Function('f', IntSort(), IntSort())

prove(Implies(x == y, f(x) == f(y)))  # Proved!

​
Unsatisfiable Cores

When a set of constraints is unsatisfiable, Z3 can identify a minimal subset responsible for the contradiction: 
from z3 import *

x = Int('x')
y = Int('y')

s = Solver()
s.set(unsat_core=True)

# Add tracked assertions
s.add(x > 10, "c1")
s.add(y > x, "c2")
s.add(y < 5, "c3")  # Contradicts c1 and c2
s.add(y > 0, "c4")

result = s.check()
if result == unsat:
    core = s.unsat_core()
    print("Unsatisfiable core:", core)
    # Output: [c1, c2, c3]

​
SMT-LIB Format

Z3 supports the standardized SMT-LIB format for portability: 
(declare-const x Int)
(declare-const y Int)

(assert (> x 10))
(assert (> y x))
(assert (< y 15))

(check-sat)
(get-model)

​
Performance Tips

SMT solving is NP-complete in general. Some tips for better performance:
  • Use appropriate theories (avoid nonlinear arithmetic when linear suffices)
  • Simplify constraints before adding them
  • Use incremental solving with push/pop
  • Set timeouts to prevent indefinite solving
  • Consider using tactics for preprocessing

Solvers

Learn about Z3’s solver interface

Expressions

Understand Z3’s expression system

Models

Working with satisfying assignments

​
References

  • SMT-LIB Standard
  • Z3 API: src/api/api_solver.cpp
  • Examples: examples/python/example.py, examples/c++/example.cpp

Build docs developers (and LLMs) love

Get started for freeTalk to us