Work around Z3 not producing models for some quantified expressions by tautschnig · Pull Request #8703 · diffblue/cbmc

tautschnig · 2025-07-31T08:38:19Z

Z3's solve_eqs preprocessor eliminates symbols whose definition contains a
quantifier, and then returns the quantified expression from get-value instead
of a value (see Z3Prover/z3#7743), which CBMC reports as an error.

The first commit defines Boolean variables with a quantified definition via
two (let-bound) implications rather than an equality when using Z3. The second
commit, with Z3, replaces each quantifier that is not nested within another
quantifier by such a Boolean variable, which also covers quantifiers that are
part of other definitions (e.g., an assignment to a non-Boolean symbol).

The third commit only refactors the SMT2 unit tests to share the converter set-up. The fourth commit covers the remaining case: a Boolean symbol that set_to defines directly by a quantifier (e.g. __CPROVER_bool b = __CPROVER_exists { ... };), which the second commit's lifting leaves alone because the quantifier is at the top level. It is now defined via the Boolean variable for the quantifier (new test z3/quantifier-boolean-definition).

The workaround applies only when the solver is known to be Z3 (--z3). With --external-smt2-solver or --outfile, which use the generic solver configuration, the single equality is still emitted.

Six Quantifiers-* tests now pass with Z3 and are no longer tagged
broken-z3-smt-backend, exists_memory_checks/smt_missing_range_check is
CORE again, and z3/Issue5977.desc again expects exactly "unknown". The
commit messages include runtimes with Z3 4.8.12: unchanged on quantifier tests
that already passed; tests that previously stopped with an error now run to
completion.

Fixes: #8679

Each commit message has a non-empty body, explaining why the change was made.
n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
My commit message includes data points confirming performance improvements (if claimed).
My PR is restricted to a single feature or bugfix.
n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

codecov · 2025-08-05T17:54:57Z

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 81.03%. Comparing base (37a17ad) to head (d3b8422).
⚠️ Report is 2 commits behind head on develop.

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #8703   +/-   ##
========================================
  Coverage    81.02%   81.03%           
========================================
  Files         1723     1723           
  Lines       191326   191408   +82     
  Branches        73       73           
========================================
+ Hits        155029   155109   +80     
- Misses       36297    36299    +2

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.

Copilot

Pull request overview

Works around a Z3 issue where preprocessing can eliminate Boolean symbols whose definitions contain quantifiers, leading to problematic get-value/model extraction behavior (e.g., quantified expressions appearing in counterexamples).

Changes:

Switch quantifier-containing Boolean “definitions” from a single equality assertion to two implication assertions (bidirectional implication) to avoid Z3’s solve_eqs substitution eliminating the symbol.
Add explanatory comments documenting why equality assertions are insufficient in this scenario.

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

Copilot · 2026-03-27T14:05:37Z

+    out << "(assert (=> ";
    convert_literal(l);
    out << ' ';
    convert_expr(prepared_expr);
    out << "))\n";
+    out << "(assert (=> ";
+    convert_expr(prepared_expr);
+    out << ' ';
+    convert_literal(l);
+    out << "))\n";


The quantified expression is emitted twice (once in each implication), which can significantly increase SMT2 output size and slow down both writing and solving for large quantified terms. Consider using a single assert that binds the quantified term once (e.g., via an SMT-LIB let) and then asserts both implications against that binding to avoid duplicating prepared_expr.

Copilot · 2026-03-27T14:05:37Z

  // Z3 refuses get-value when a defined symbol contains a quantifier.
+  // Using (assert (= ...)) doesn't help because Z3's solve_eqs
+  // preprocessor eliminates the symbol by substituting the quantified
+  // expression. Using bidirectional implication instead prevents this.
  if(has_quantifier(prepared_expr))


This change is intended to address a Z3 model/get-value regression involving quantified terms, but the PR description indicates no regression test is included. Please add or update a regression test (e.g., in regression/cbmc/z3/) that reproduces #8679 on affected Z3 versions and demonstrates the workaround prevents quantified terms from appearing in get-value responses / keeps traces readable.

Z3's solve_eqs preprocessor eliminates a Boolean symbol defined via (assert (= symbol <quantified-expr>)) by substituting the quantified expression, and then returns that quantified expression from get-value instead of a Boolean value, which CBMC cannot parse (see Z3Prover/z3#7743). Emit the equivalence as two implications, (=> symbol <expr>) and (=> <expr> symbol), which solve_eqs does not treat as an elimination opportunity, while preserving logical equivalence. A let-binding shares the quantified expression so that it is emitted only once. As this is a Z3-specific problem, the workaround is gated on the Z3 solver; other solvers keep the single equality assertion. Z3 >= 4.15.3 offers the opt-in option smt.solve_eqs.non_ground (default: true), which avoids this elimination when set to false, but Z3's default behaviour is unchanged and older versions reject the option. The workaround applies when the solver is known to be Z3 (--z3). With --external-smt2-solver or --outfile, which use the generic solver configuration, the single equality is still emitted. This reinstates regression/cbmc-primitives/exists_memory_checks/smt_missing_range_check as CORE: it was demoted to KNOWNBUG in b0eedde precisely because of this Z3 misbehaviour. Likewise, regression/cbmc/z3/Issue5977.desc again expects exactly "unknown", and Quantifiers-assertion, Quantifiers-initialisation2, and Quantifiers-two-dimension-array now pass with Z3 and are no longer tagged broken-z3-smt-backend. A unit test in unit/solvers/smt2/smt2_conv.cpp additionally pins the exact SMT2 output for both Z3 and other solvers. Quantifiers that reach Z3 via other definitions, such as an assignment to a non-Boolean symbol, are handled in the next commit. Runtime of `cbmc --z3` (Z3 4.8.12) is unchanged on the quantifier tests that already passed before. Tests that previously stopped with an error right after the first solver call now run to completion, e.g., Quantifiers-initialisation2 takes 11.9s (previously an error after 1.4s). Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

The previous commit makes Z3 return Boolean values for variables that are defined via a quantified expression. Quantifiers may also be part of other definitions, such as an assignment to a non-Boolean symbol (in `int x = __CPROVER_forall { ... };`, x is defined via an if-then-else over the quantifier), or of Boolean definitions that use define-fun. Z3's solve_eqs preprocessor eliminates these symbols, too, and then returns quantified expressions from get-value. With Z3, now replace each quantifier that is not nested within another quantifier by a fresh Boolean variable, defined using the encoding of the previous commit, so that no other definition contains a quantifier. Quantifiers-assignment, Quantifiers-if, and Quantifiers-not now pass with Z3 and are no longer tagged broken-z3-smt-backend. Their runtime with Z3 4.8.12 is 11.5s, 0.14s, and 0.14s, respectively (previously, these stopped with an error after 5.3s, 0.09s, and 0.09s). Quantifiers-not-exists/fixed.desc remains broken with Z3: it now reports an error after 83s, previously after 0.09s. Fixes: diffblue#8679 Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

`get_assert`, `get_assert_with_datatypes`, and `convert_handle` each set up a symbol table, namespace, output stream, and `smt2_convt`. Use a single helper, parameterised by the solver and the action to apply to the converter, so that further SMT2 unit tests do not add more copies. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

With Z3, prepare_for_convert_expr replaces each quantifier by a Boolean variable, except for a quantifier at the top level, as that is what convert uses to define such a variable. When set_to defines a symbol by a quantifier, as is the case for `__CPROVER_bool b = __CPROVER_exists { ... }`, the definition `(= b <quantifier>)` was emitted as is. Z3's solve_eqs then eliminates b, and get-value on Boolean variables that depend on b returns quantified terms ("non-constant value for variable B13", VERIFICATION ERROR, with Z3 4.8.12 and 4.15.4). Define such symbols via the Boolean variable that convert introduces for the quantifier. The new regression test z3/quantifier-boolean-definition reported VERIFICATION ERROR before; a unit test pins the emitted SMT2 for Z3 and other solvers. Co-authored-by: Kiro <kiro-agent@users.noreply.github.com>

tautschnig self-assigned this Jul 31, 2025

tautschnig force-pushed the trying-to-fix-z3-with-quantifiers branch from b77cf1c to e92bda3 Compare August 5, 2025 17:26

tautschnig mentioned this pull request Aug 12, 2025

Quantifier failure in loop invariant model-checking/kani#4282

Open

tautschnig mentioned this pull request Aug 20, 2025

Quantifier failure for arbitrary range model-checking/kani#4310

Open

tautschnig force-pushed the trying-to-fix-z3-with-quantifiers branch from e92bda3 to bfa6d2d Compare March 26, 2026 18:35

tautschnig marked this pull request as ready for review March 27, 2026 14:01

Copilot AI review requested due to automatic review settings March 27, 2026 14:01

tautschnig requested review from TGWDB, kroening, martin-cs and peterschrammel as code owners March 27, 2026 14:01

Copilot started reviewing on behalf of tautschnig March 27, 2026 14:01

View session

Copilot AI reviewed Mar 27, 2026

View reviewed changes

tautschnig force-pushed the trying-to-fix-z3-with-quantifiers branch from bfa6d2d to 06be21e Compare May 28, 2026 10:46

tautschnig force-pushed the trying-to-fix-z3-with-quantifiers branch from 06be21e to 4e093d1 Compare June 14, 2026 21:50

tautschnig force-pushed the trying-to-fix-z3-with-quantifiers branch 2 times, most recently from 05b6978 to 2887c27 Compare November 6, 2026 18:24

tautschnig mentioned this pull request Nov 6, 2026

SMT2: compare arrays only on the indices below their size #9230

Open

4 tasks done

tautschnig and others added 4 commits November 13, 2026 15:27

tautschnig force-pushed the trying-to-fix-z3-with-quantifiers branch from 2887c27 to d3b8422 Compare November 13, 2026 15:42

Navigation Menu

Repository navigation

Work around Z3 not producing models for some quantified expressions - #8703

Work around Z3 not producing models for some quantified expressions#8703
tautschnig wants to merge 4 commits into
diffblue:developfrom
tautschnig:trying-to-fix-z3-with-quantifiers

tautschnig commented Jul 31, 2025 •

edited

Loading

Uh oh!

codecov Bot commented Aug 5, 2025 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

Copilot AI Mar 27, 2026

Uh oh!

Copilot AI Mar 27, 2026

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

tautschnig commented Jul 31, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

codecov Bot commented Aug 5, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Codecov Report

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Uh oh!

Copilot AI Mar 27, 2026

Choose a reason for hiding this comment

Uh oh!

Copilot AI Mar 27, 2026

Choose a reason for hiding this comment

Uh oh!

This branch has not been deployed

Reviewers

Uh oh!

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

tautschnig commented Jul 31, 2025 •

edited

Loading

codecov Bot commented Aug 5, 2025 •

edited

Loading