• Encode your problem as a proposition that the SMT solver can check.

• Run the SMT solver, by checking if the proposition is satisfied.

• If that is true, then a model (a truth assignment) is found, you should now turn that back into a (counter -) solution the user can understand.

N-Queens

import z3
import itertools


def at_most_one(props):
    conditions = []
    for p, q in itertools.permutations(props, 2):
        conditions.append(z3.Or(z3.Not(p), z3.Not(q)))
    return z3.And(*conditions)


columns = "abcd"
rows = "1234"

# Create a boolean for each possible queen location.
queen_on_square = [[z3.Bool(f"Q{c}{r}") for c in columns] for r in rows]
s = z3.Solver()

# There need to be exactly one queen per row.
for ir, r in enumerate(rows):
    row = [queen_on_square[ic][ir] for ic, c in enumerate(columns)]
    s.add(z3.Or(*row))
    s.add(at_most_one(row))

# There can be at most one queen per column.
for ic, c in enumerate(columns):
    column = [queen_on_square[ic][ir] for ir, r in enumerate(rows)]
    s.add(at_most_one(column))

# There can be no more than one queen per diagonal.
prim, secd = [[] for r in row * 2], [[] for c in column * 2]
for ir, r in enumerate(rows):
    for ic, c in enumerate(columns):
        # primary diagonals are constant over subtraction
        prim[ir - ic].append(queen_on_square[ic][ir])
        # secondary diagonals are constant over summation
        secd[ir + ic].append(queen_on_square[ic][ir])

for diag in prim + secd:
    s.add(at_most_one(diag))

# This is kind of an ugly hack.
assert str(s.check()) == "sat"

model = s.model()

for ir, r in reversed(list(enumerate(rows))):
    print(f" {r} ", end="")
    for ic, c in enumerate(columns):
        is_black = (ir + ic) % 2 == 0
        if is_black:
            print("\033[40m\033[37m ", end="")  # ]]
        else:
            print("\033[47m\033[30m ", end="")  # ]]
        has_queen = bool(model[queen_on_square[ic][ir]])
        print("♛" if has_queen else " ", end="")
        print(" \033[0m", end="")  # ]
    print()
print(f"    {'  '.join(columns)}")

Remember to simplify

>>> i = z3.Int("i")
>>> for r in range(10):
...     i = i + 1
... 
>>> print(i)
i + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1 + 1

>>> i = z3.Int("i")
>>> for r in range(10):
...     i = z3.simplify(i + 1)
... 
>>> print(i)
10 + i

int incr(int a) { 
  int x = a;          // []                    |- x := a
  if (x > 10) {       // [a > 10]              |- x := a
    x =+ 1;           // [a > 10]              |- x := a + 1
    if (x < 10)       // [a > 10, a + 1 < 10]  |- UNSAT
      assert false;   // never executed
  }
  return x;           // returns [ a  > 10 |- a + 1 
                      //         , a <= 10 |- a      ]
}

But how do we handle loops?

We don't... Bound the depth of the execution

stack : list[tuple[PC, SymState, SymPath, int]]

def step(pc: PC, state: SymState) 
  -> Iterable[PC, SymState, SymPath]]: ...

def analyse(pc : PC, inputs : list[tuple[str, JvmType]], max_depth : int):
  # assuming only integers, create symbolic vars for all input
  locals = z3.Ints(" ".join(i_name for i_name, _ in inputs))
  # create state.
  state = SymState.from_locals(locals)

  # Create a stack to do depth first search with.
  stack : list[tuple[PC, SymState, SymPath]] = [(pc, state, [])]

  # As long as the stack is not empty
  while stack:
    # pop the end of the stack
    (pc, state, path, n) = stack.pop(-1)

    # Check if state does something we want to warn the user about.
    if interesting(state):
      return "found interesting state"

    # otherwise create the list of next branches 
    for (pc, state_, pathc) in step(pc, state):
        # add new path constraints to the path
        path_ = path + pathc

        # check if path is reachable
        if str(z3.check(path_)) != "sat": 
          continue

        # append stack if within limits
        if n < max_depth:
          stack.append((pc, state_, path_, n + 1))

  return f"all is fine, uptil depth {max_depth}"