Satisfiability Modulo Theories

Concept

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.

First seen 5/25/2026

Last seen 5/25/2026

Evidence 1 chunks

Wiki v1

WIKI

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

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

LINKED ENTITIES

2 links

UCLID5 APPLIES Extracted graph relationship

Z3 SOLVES The evidence identifies Z3 as an SMT solver developed at Microsoft Research and used in the cited work.

CITATIONS

7 sources

7 citations — click to expand

[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