Automated verifiers rely on SMT solvers as a backend for proof automation. This simplifies verification in the common case, but also creates usability challenges due to instability. Previous work proposes mitigation strategies motivated by the assumption that instability is a fundamental theoretical limitation. We conjecture that the instability experienced by verifiers today is often caused by fixable engineering problems, and is thus not fundamental. Should this be true, the more consequential approach to addressing instability would be to identify root causes and connect them with solver improvements. We conducted case studies on 11 deemed-unstable queries from existing verification projects and from issues reported on the Z3 repository, with the goal of diagnosing the root causes of instability. For all of them, instability is attributable to solver bugs, misconfiguration, or misaligned expectations. We present our analysis and draw conclusions regarding better instability metrics, interfaces that make instability explicit, systematic debugging methods, and easier-to-debug SMT solvers.
Formal verification often relies on SMT solvers as a backend for proof automation. In the common case, SMT solvers significantly lower the amount of efort and expertise required for verification, as they discharge most proofs quickly.
Yet, SMT-based verifiers face significant usability challenges. A major reason is that SMT solvers
sufer from instability, whereby minor changes to the input query, such as addition or removal of
redundant constraints, can have disproportionate efects on performance, or even the outcome (e.g.
turn an unsat into an unknown). Recent work has shown that even purely syntactic mutations such as
renaming variables or reordering assertions can have such efects [
Existing (and ongoing) work [
We formulate a conjecture that the instability experienced by verifiers today is mostly caused by ifxable engineering problems, not fundamental theoretical limitations. SMT is combinatorially hard, so solvers must rely on heuristics to be eficient: in that sense, instability may be inescapable. However, we speculate that, in the context of a finite set of existing tools and their encodings, the heuristics that already work well (albeit sometimes unstably) can be made stable through dedicated engineering.
Motivated by this conjecture, we set out to investigate the root causes of instability. The SMT
community does not have the tools and techniques today to pinpoint root causes at scale, generically,
and automatically. In lieu of this and as a starting point, we manually examined a handful of queries in
detail. We conducted case studies on 11 queries that were unstable with Z3 [
In all 11 case studies, we found that the heart of the problem was neither a bad encoding nor bad
luck. Rather, they boiled down to concrete, fixable root causes:
• 6 of the queries were unstable due to bugs in the solver (§4.1). We have implemented three bug
ifxes addressing all 6 queries, which have been merged upstream.
• 2 were unstable due to misconfiguration (§4.2). These are each stabilized by a solver parameter
that is set through the command line. In both cases, the parameter’s efect is intuitive and its
necessity is obvious in hindsight.
• 3 were unstable due to misasligned expectations (§4.3), specifically relating to how triggers are
treated in the presence of relevancy filtering [
In this section we define instability, and discuss recent eforts towards mitigating it. Then, we present an overview of a CDCL(T)-based SMT solver’s architecture and operation, highlighting the aspects most relevant to our discussion. We focus specifically on Z3, as it is the solver we used in our case studies.
Proof instability, also called brittleness [
Recent work has proposed various measures to reduce instability. One general direction is to
pre-process queries, to simplify [
This section presents an overview of Z3’s architecture and operation, using the following query as a running example:
( < 0) ∧ ( < 0) ∧ (( + > 0) ∨ ( · < 0))
Z3 comprises a CDCL(T) core, and a set of theories. The former is essentially a SAT solver that treats theory atoms (e.g., ( < 0), ( + > 0)) as independent boolean variables and aims to construct a boolean model that satisfies the propositional constraints (e.g., {( < 0) :− true, ( < 0) :− true, ( + > 0) :− false, ( · < 0) :− true}). Theories are mainly responsible for ensuring that the set of propositional assignments in the model is consistent with respect to theory semantics. For this model, the theory of arithmetic would raise a conflict: ( < 0) :− true, ( < 0) :− true, and ( · < 0) :− true cannot simultaneously hold.
The CDCL(T) core makes decisions on propositional assignments one by one, either through boolean constraint propagation (BCP) or by branching. After each round of decisions, it performs theory propagation to see if the current (partial) model is consistent with the theories. In this example, before any branching, it decides that any model must have ( < 0) :− true and ( < 0) :− true through BCP, as these appear as unit clauses. Then, it propagates both assignments to the theory of arithmetic, which says that the model is consistent. When there is no unit clause left to be propagated, Z3 branches on a decision, creating a backtracking point. Let’s assume that it first decides to explore the case where ( + > 0) := true. As soon as this decision is theory-propagated, the theory of arithmetic raises a conflict. In response, the CDCL(T) core backtracks to the previous partial model, and augments it with ( + > 0) := false. Finally, the CDCL(T) core decides ( · < 0) :− true (through BCP), which causes another arithmetic conflict. As the CDCL(T) core cannot backtrack anymore, it decides that the query is unsat.
Z3 refines the basic CDCL(T) architecture with many heuristics and optimizations. One that is
particularly important in the context of this paper is relevancy filtering [
Another important mechanism to highlight is trigger-based quantifier instantiation , also called
E-matching. We do not present E-matching here, and instead refer to prior literature [
We have conducted case studies over 11 unstable queries. 4 of these were produced by early versions
of TPot [
We did not choose the queries for our case studies systematically. Instead, we started with examples we organically came across and were puzzled by. Then, we investigated issues that were recently raised with Z3 developers or directly shared with us, as well as some of the simpler queries in the Mariposa benchmark.
We used Z3 builds between versions 4.13.4 and 4.14.2 for all of our case studies.
TPot raw [
SMT solvers, like all software, have bugs. It is well-known [
We have identified and fixed three bugs that lead to instability in Z3. All three patches have been merged upstream. (declare-fun loc ((_ BitVec 64)) Int) mdata: struct metadata page aligned (declare-fun addr_mdata () (_ BitVec 64)) bytes..[.0+:8] p: char * ... (((dddeeeccclllaaarrreee---fffuuunnn maaddradrtra_(a)(r)r(A((rA)rrar(y_ayIBniIttnVt(_ec(_B6iB4t)iV)teVce8c)8)))))
arr: char[] ;(demcdlaatrae-ifsunpafge((a_liBginteVdec 8)) Int)
arr[0] arr[
assert mdata[0+:8] == addr_arr (a) initial state ; the assumption
assert f(arr[
(5): p == addr_arr ==> loc(p) == loc(addr_arr) ;[B] ;(6)(:4)p, !(=5)addr_arr
• patch-dynack fixes a bug that kept dynamic Ackermannization axioms (see §4.1.1) from being propagated to theories properly and that caused the relevancy of certain atoms to be forgotten during backtracking. • patch-fixedeq fixes relevancy tracking for equality lemmas between bitvectors that are assigned the same value by the bitvector theory, such that the equality is propagated to the egraph structure. • patch-mbqi fixes a bug related to model-based quantifier instantiation for uninterpreted sorts with finite domains, whereby Z3 would complete partial functions models with arbitrary values. patch-dynack and patch-fixedeq are bugs that afect the communication between the CDCL(T) core and the theories. This is a channel that is regulated by relevancy filtering, and can easily keep the solver from finding the intended proof. Section §4.1.1 presents patch-dynack in detail.
We discovered the bug related to patch-dynack while experimenting with an early version of TPot, when the solver got stuck on the raw query. This was an instance of instability: raw mostly comprised the same assertions as previous queries TPot made on the same symbolic execution path, and used the same logic (quantifier-free bitvectors and arrays), so we expected Z3 to discharge the query with similar reasoning.
Fig. 1 presents a simplified (and still unstable) version of the query, along with the context that produced it and the sketch of an intended proof. The original query included 86 assertions spanning 3600 lines of SMT2. The proof sketch justifies why we expect the query to be easily solvable, and helps explain how the bug leads to explosion. We have found writing pen-and-paper proof sketches to be helpful for debugging as well.
Dynamic Ackermannization [
While Ackermannization itself worked as expected for the query, a Z3 bug related to the interaction between Ackermannization and relevancy filtering kept step (6) from proceeding: Ackermannization would create fresh literals for step (5) (e.g., p == addr_arr) without marking them as relevant. This efectively made the Ackermann clauses invisible to the theories, so the theory of arithmetic would not learn that assuming p == addr_arr propagates loc(p) == loc(addr_arr). Consequently, it would not learn that p != addr_arr.
When Z3 backtracks it will retain certain axioms (i.e., theory lemmas, including Ackermann axioms) but forget about their relevancy. So the lifetime of the lemma is not scope-bound, but its relevancy is. This essentially results in the axioms only participating in propositional propagation (within the CDCL(T) core), but not theory propagation. This behavior is intended if the solver creates theory axioms using existing literals, but works against leveraging theory axioms with fresh literals across backtracking points.
Solvers come with many configurable parameters that toggle heuristics, determine thresholds, set resource limits, and so on. The current version of Z3 (4.14.2) has 657 parameters configurable through the command line. Intuitively, the configuration should play a role in whether the solver behaves as expected consistently for an encoding scheme; indeed, two of our case studies turned out to be configuration issues.
; a, b, arr, i are bitvectors of size 32 assert b = arr + <elem_sz> * i assert a + 200 <= b assert a + 100 >= b lemma lemma_2toX() ensures power2(64) == 18446744073709551616; ensures power2(60) == 1152921504606846976; ensures power2(32) == 4294967296; ensures power2(24) == 16777216; ensures power2(19) == 524288; ensures power2(16) == 65536; ensures power2(8) == 256; { } reveal_power2();
bv_rewrite.smt2 is a minimized (to 14 lines) version of an unstable query that was produced by TPot. It involves 4 variables, all of which are bitvectors of size 32. As shown in Fig. 2, the time it takes Z3 to solve bv_rewrite.smt2 depends heavily on a bitvector coeficient ( elem_sz) appearing only in an assertion that is redundant and therefore should be inconsequential.
With the default configuration, Z3 determines that the query only involves quantifier-free constraints over bitvectors, and so it is essentially a boolean satisfiability problem. Then Z3 decides to bit-blast the query, representing each bit with a boolean variable, and discharge it using the built-in SAT solver (which is separate from the CDCL(T) core), without ever involving the actual SMT solver. Using the command line argument tactic.default_tactic=smt prevents this from happening and makes Z3 terminate instantly irrespective of the coeficient.
lemma_2toX.smt2 is a query produced by Dafny to prove the lemma in Fig. 3, as a part of the
IronFleet [
In the SMT encoding, Dafny represents power2 with an uninterpreted function, and provides the
usual [
The problem is that the global threshold Dafny sets on quantifier instantiation depth
(smt.qi.eager_threshold=100) is too small to fully unfold power2(64). We have empirically
observed using SMTScope [
The misconfiguration here is obvious in hindsight. In practice, it was not easily noticable as it made the query unstable, not consistently unknown. This is because when we get lucky, Z3 reuses unfoldings that were used to close branches corresponding to the last five ensures to close the first two as well. So whether Z3 returns unsat or unknown depends on the order in which it explores diferent branches. Setting the threshold to 200 allows all branches to close in isolation and stabilizes the query.
One may also configure Z3 such that quantifier instances are efectively shared across branches, by disabling relevancy filtering ( smt.relevancy=0). Doing so indeed stabilizes this particular query, but makes most other Dafny queries to explode, due to Dafny’s quantifer-heavy encoding.
Developers of SMT-based verifiers treat solver optimizations as black boxes that are only relevant as far as performance is concerned. They assume that, barring timeouts and resource limits, toggling an optimization may change the solver’s performance but not its completeness (e.g., may not turn an unsat into an unknown), otherwise the solver must have a bug. This assumption is incorrect, at least in the case of relevancy filtering combined with trigger-based quantifier instantiation.
Our case studies include two queries with unstable outcomes for which the root cause is a mismatch between how verifier developers expect triggers to be treated and how Z3 treats them in the presence of relevancy filtering. These are not Z3 bugs; relevancy filtering behaves according to how it is specified, through semantic tableau rules, even though it violates user expectations. In §4.3.1 we present a minimal reproduction and in-depth discussion on this mismatch.
Consider the query in Fig. 4. The query is clearly unsat, as instantiating the quantifier with :− 0
trivially contradicts the first assertion. The conventional understanding of triggers, as described by
Leino and Pit-Claudel [
The core of the problem is that there is a branch of the proof that does not close itself; it depends on the quantifier instance but does not trigger instantiation. In the branch where (0) is false and (0) is true, Z3 considers (0) to be an irrelevant disjunct in (or (A 0) (B 0)), as its truth value does not afect the value of the disjunction. Therefore, Z3 keeps the assignment (0) :− false from being propagated to any theory, including the E-matching engine. So, the branch only closes if Z3 visits one of the branches that triggers instantiation (e.g., (0) :− true, (0) :− false) before this one and reuses the instance.
Another way to understand the problem is to realize that relevancy filtering efectively simulates tableau-search, whereby the solver structurally branches on the problem. In this example, the solver looks at the first assertion and branches on satisfying (0) versus (0). The latter branch is essentially equivalent to solving a version of the query with (0) omitted from the first assertion, and that version should be unknown according to Leino and Pit-Claudel’s description.
The query’s success depends purely on the branching order and 50% of branching orders lead to success. We experimented with 8 variants of the query, changing the polarities of (0) and (0), and toggling the pattern between () and ().
Some of these seemed to be consistently unsat or unknown irrespective of the random seed, suggesting that these variations play a role in the query’s success. On closer look, some variations may fix a branching order with Z3’s default configuration: Z3 will always guess false for the first atom it branches on irrespectively of the random seed (the actual guessing process - phase caching - is somewhat more involved, but the caches are initialized to false). Also, the way Z3 chooses the first atom to branch on involves randomness but it is not uniformly random. To work around these issues, we made a surgical modification on Z3’s source code to set the frequency of randomized case splits to 1.00 (the default is 0.01). This frequency is hard-coded and is not configurable through the command line. We then ran Z3 with smt.phase_selection=5 (random).
Assignment 1 branch? literal relevant?
Assignment 2 branch? literal relevant? yes
A(0) ¬A(0) B(0) ¬B(0) yes no yes no no yes no
B(0) A(0) ¬A(0) A(0) yes no no yes Total:
Result unsat unknown unknown unknown unsat unsat unknown
Probability 1/4 1/4 1/8 1/8 1/4 1/2 1/2
In this section, we discuss our experience with the case studies. We hope the lessons we learned will inform future work on addressing instability.
In §4.3.2, we describe how certain variations on the query in Fig. 4 seem to have implications on stability, when in fact all they do is resample a random distribution that is unafected by the random seed. For this query, the order of disjuncts, and the symmetric choice of the trigger term between the two disjuncts, are sources of randomness. This is an example of how having multiple sources of randomness can lead to confusion while identifying and debugging instability.
Another such example is the IfNorm0 query. The original query produced by Dafny succeeds with all random seeds, but asking Dafny to normalize the names of functions and variables (through a Dafny command line option) makes the query explode with all random seeds. This pattern is confusing, as it suggests that normalization is to blame for instability. The pattern occurs because Z3 reorders disjunctions using a name-dependent order and Dafny sets the smt.case_split=3 parameter, which orders case splits structurally, starting from the leftmost disjunct. This makes the case split order insensitive to the random seed, but sensitive to variable and function names.
Ensuring that all randomness is controllable through an explicit random seed would be a step towards making instability easier to identify and address.
Existing approaches to examining Z3 traces [
We adopted a methodology, which we think can be largely automated, based on comparing solver traces using standard text dif tools. Given an unstable query, we could often find a “good” configuration (of solver parameters, variable names, etc.) that produces the expected behavior. When a good configuration does not appear organically, we had success with parameter fuzzing or randomness fuzzing through Mariposa. We then difed the trace from a good run against one from a bad run, identified the first point of divergence, and made surgical modifications on the Z3 source to unify the solver’s behavior over the two. Of course, the first point of divergence usually was not itself related to the root cause, but repeating this process until both configurations succeed allowed us to discover particularly elusive bugs.
This methodology would be greatly simplified if we were able to modify and replay solver traces. This would allow us to unify behavior without having to modify the solver’s source code. Beyond trace difs, replaying traces would make it much easier to test hypotheses of the form “had been done diferently, the query would not have exploded”.
We also note that we used the tracing mechanism built into Z3, which was built for VCC, and not tailored for our purpose. There are many relevant steps that do not get logged (e.g. theory propagations, the state of the egraph, relevancy), which sometimes hides root causes and makes it hard to unify the next point of divergence. 5.3. Proof sketches §4.1.1 uses a proof sketch to explain the root cause of instability for a simplified version of the raw query; we wrote similar sketches for most case studies. In our experience, writing down such pen-and-paper proof sketches and trying to identify what keeps the solver from finding them has been useful for debugging, as well as explaining root causes after the fact to convince oneself that the “right problem” was fixed. We believe debugging tools that ingest proof sketches along with solver traces and pinpoint the missing proof step would have greatly simplified our case studies.
Debugging instability through proof sketches mimics how one debugs functional correctness problems in most classes of software: by having a clear picture of the expected behavior and iteratively narrowing down where the program departs from it. Without proof sketches, this is only possible for SMT solvers at two extreme granularities, neither practical. On one extreme, one may say the expected behavior is simply “the solver must return unsat quickly”. This does not allow for iteratively narrowing down on the problem beyond the solver’s interface. Debugging at the interface by giving the solver iteratively simplified/reduced versions of the query and trying to deduce which simplification step caused the problem often leads to ill-informed and misleading conclusions. On the other extreme, one may examine solver traces. This requires the developer to be intimately familiar with the solver’s internals and even then they are often too large and too low-level to be practically understood by humans. Importantly, traces also mostly consist of “dead ends”, i.e., branches explored and axioms instantiated by the solver as part of proof search that ultimately do not make progress towards the expected proof, and are uninteresting in pinpointing the divergence from expected behavior.
Proof sketches can be written at arbitrary granularity, and deepened only in steps that need to be narrowed down on (e.g., Fig. 1 elides the bitvector and arithmetic axioms that need to be involved for steps (8) and (10); the solver follows these steps as expected so the user does not need more detail). This makes proof-sketch debugging scale well with the size of the query being debugged. The original raw query spans 55× the number of SMT lines the simplified version in Fig. 1 does, but its proof sketch still consists of 10 (considerably bigger) steps.
We conjecture that the instability experienced by SMT-based verifiers today is mostly caused by fixable engineering problems, not fundamental theoretical limitations. We support this conjecture with 11 case studies, which identified three classes of root causes: solver bugs, misconfigurations, or misaligned expectations. We hope our experience will inform future work on addressing instability in three ways. First, some of the unstable queries we studied were not flagged as such by existing metrics; we argue for an instability metric that reflects user experience. Second, part of our debugging methodology can be automated, and would greatly benefit from tool support for debugging through proof sketches, and replaying solver traces. Third, having multiple sources of randomness makes instability debugging harder, so unifying all random behavior under explicit random seeds would be a step forward.
This material is based upon work supported by the Air Force Research Laboratory (AFRL) and Defense Advanced Research Projects Agencies (DARPA) under Contract No. FA8750-24-C-B044. Any opinions, ifndings, and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the AFRL and DARPA.
The authors did not use any generative AI tools in the writing of this paper.