Skip to content
STIMSMITH

Satisfiability Modulo Theories

Concept WIKI v1 · 5/25/2026

Satisfiability Modulo Theories (SMT) is used in UCLID5-based formal verification to solve verification-condition formulas expressed over multiple data-type theories. In the cited UCLID5 workflow, an SMT solver returns unsatisfiable, satisfiable, or indeterminate results, which UCLID5 interprets respectively as a proved verification condition, a likely failed condition with a counterexample, or an unresolved proof attempt.

Overview

Satisfiability Modulo Theories (SMT) appears in the UCLID5 verification workflow as the solving step for verification conditions. UCLID5 generates verification conditions from a model and verification script as formulas in a logic that supports the multiple data types—called theories—used in the model. These formulas are typically the negations of the properties that the user wants to verify, and UCLID5 then invokes an SMT solver on them. [C1]

Role in UCLID5 verification

In the cited processor-verification workflow, models may use multiple forms of typed data, including uninterpreted functions and arrays with arbitrary index and data types. The combination of the model and verification script is translated by UCLID5 into verification-condition formulas over the relevant theories. [C2]

UCLID5 can use several different SMT solvers. In the cited work, the authors used the Z3 solver developed at Microsoft Research. [C3]

Solver outcomes

When UCLID5 invokes an SMT solver, the solver can return three kinds of answers: [C4]

  1. Unsatisfiable: Because the formulas are typically negations of desired properties, an unsatisfiable result indicates that the desired verification condition holds. [C4]
  2. Satisfiable: The solver provides concrete values for all data elements in the formula, including uninterpreted functions, such that the formula holds. This typically indicates that a verification condition failed. UCLID5 uses these values to generate a counterexample: a sequence of model actions that could violate the verification condition. [C5]
  3. Indeterminate: The solver cannot find a satisfying solution but also cannot prove the formula unsatisfiable. This typically indicates that the model is too complex or requires more sophisticated reasoning than the solver can provide. [C6]

Counterexample interpretation

A satisfiable SMT result in this workflow is not described merely as a Boolean failure. UCLID5 uses the solver-provided concrete values to construct a counterexample, and such counterexamples can indicate one of several issues: a true design error, an inaccurate or overly abstract model, or an improperly expressed verification condition. [C5]

Modeling implications

The cited workflow emphasizes that choosing data types and abstractions affects verification. The authors state a general rule: use the most abstract model possible that still captures the system properties needed for correctness. Different pipeline variants may require different abstraction levels during verification. [C7]

LINKED ENTITIES

2 links
UCLID5 APPLIES
Z3 SOLVES

CITATIONS

7 sources
7 citations
[1] UCLID5 generates verification conditions as formulas in a logic supporting multiple data-type theories, typically as negations of properties to verify, and invokes an SMT solver. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] The cited modeling workflow uses typed constructs such as uninterpreted functions and arrays with arbitrary index and data types. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] UCLID5 can use several SMT solvers, and the cited work used the Z3 solver developed at Microsoft Research. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] An SMT solver invoked by UCLID5 can return unsatisfiable, satisfiable, or indeterminate; an unsatisfiable result on a negated property indicates that the desired verification condition holds. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] A satisfiable SMT result provides concrete values for data elements, including uninterpreted functions, and UCLID5 uses these values to generate a counterexample; such counterexamples can indicate a design error, an inaccurate or overly abstract model, or an improperly expressed verification condition. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[6] An indeterminate solver result means the solver found no satisfying solution but could not prove unsatisfiability, typically because the model is too complex or requires more sophisticated reasoning. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[7] The cited report recommends using the most abstract model possible that still captures the properties needed for correctness, and notes that different pipeline variants require different abstraction levels. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5