Skip to main content

Caesar 3.0: Better Reasoning with Limited Functions

· 5 min read
Philipp Schroer
Philipp Schroer
Caesar Developer

Caesar 3.0 improves the SMT reasoning capabilities of Caesar, making verification more powerful, stable, and predictable. This release marks the conclusion of a project that started more than 9 months ago, including a successful Master's thesis by Emil-Beothy Elo.

Overview:

  1. Limited Functions
  2. Other SMT-related Improvements
  3. Other Improvements

Limited Functions​

The most important change in Caesar 3.0 is the introduction of limited functions, which are enabled by default. This is a change in how definitional func are translated into SMT. Whereas we previously translated definitional functions by using the "obvious" encoding, as uninterpreted functions and an axiom for its definition, we now guide the SMT solver by encoding fuel.

Prior to this change, coupon-collector benchmark manually encoded this idea as part of a series of declarations to define harmonic numbers:

func harmonic(n: UInt): UReal
func harmonic0(n: UInt): UReal
axiom harmonic_def forall n: UInt.
    (harmonic(n) == ite(n==0, 0, (1/n) + harmonic0(n-1)))
axiom harmonic_zero forall n: UInt.
    (harmonic(n) >= 0)
axiom harmonic0_zero forall n: UInt.
    (harmonic0(n) >= 0)

Now, we simply write:

func harmonic(n: UInt) : UReal = ite(n==0, 0, (1/n) + harmonic(n-1))

and Caesar does the rest automatically, with additional improvements:

  • Caesar generates appropriate triggers to guide the SMT solver.
  • Caesar generates an additional synonym axiom, which is actually crucial to prevent spurious counter-examples.

Our implementation supports a wide variety of options, which are documented in the debugging documentation.

  • Function Encodings, can be set via the --function-encoding command-line option:
    • axiomatic: The old encoding, which naively encodes the function as an uninterpreted function and adds an axiom for its definition.
    • decreasing: Like axiomatic encoding but only allows decreasing instantiations, where the defining axiom is only instantiated based on occurrences of the function it defines, not other functions in the definition.
    • fuel-mono: Add a version of the function for each fuel value (f_0, f_1, ...) and recursive calls decrease the fuel value.
    • fuel-param (default): Add a symbolic fuel parameter to the function.
    • define-fun-rec: Uses SMT-LIB's define-fun-rec to encode functions.
  • Fuel Values: The fuel-based encodings allow the user to specify a maximum fuel value via the --max-fuel command-line option. The default is 2.
  • Literals: The fuel-mono and fuel-param encodings have variants that additionally allow unbounded computations in the SMT solver with literal values.
  • Quantifier Instantiation Strategies: Users can now disable MBQI with --qi e-matching. When combined with the fuel-based encodings, we have termination guarantee for the quantifier instantiation strategy.
  • No Synonym Axiom: The --no-synonym-axiom command-line option can be used to disable the generation of the synonym axiom. This might lead to spurious counter-examples (unsound!), but sometimes this is acceptable or even desired.

We also support the use of limited functions in combination with uninterpreted functions. For this, we added a new @computable annotation, which can be used to mark uninterpreted functions that are computable when given literal parameters.

These changes were made possible by the work of Emil-Beothy Elo in his Master's thesis and his pull request #54.

Caesar now performs dependency tracking for SMT queries—meaning it analyzes which declarations (such as functions, axioms, and domains) are actually needed for each verification task and only includes those in the SMT query — reducing the number of declarations sent to the SMT solver. Previously, Caesar would send all declarations in the HeyVL file to the SMT solver, which could cause performance issues even when these declarations were irrelevant to the current verification task. This optimization is particularly beneficial when verifying individual procedures in files containing declarations that could interfere with counter-example generation. Now, only declarations that are actually relevant to the specific verification task are included in SMT queries.

  • As a side-effect, we now disallow axioms that do not mention any domain or func, as these would never be included in SMT queries. If such an axiom is present, Caesar will emit an error indicating that the axiom is ignored because it is not relevant to any verification task.

We updated Z3 to version 4.15.1, and now set Z3's smt.arith.nl.order to false. Many other Z3 options have been tweaked to improve quantifier instantiation stability and performance.

  • We now set the default quantifier weight to 1 instead of 0, which now aligns with the defaults used by other SMT solver integrations and APIs.
  • Caesar now emits quantifier IDs for all quantifiers, making it easier to trace and debug quantifier instantiations in SMT solver outputs.

Caesar 3.0 adds some new debugging tools for Z3's SMT reasoning.

  • --z3-seed allows users to set a seed for Z3. This is useful for debugging verification brittleness.
  • --z3-qi-profile will print Z3's quantifier instantiation statistics to the console.
  • --z3-mbqi-trace will print Z3's model-based quantifier instantiation trace to the console.
  • --z3-verbose allows users to set Z3's verbosity level.

Other Improvements​

This release also features rewritten documentation for the induction-based proof rules and minor improvements in various other places.

We re-organized and extended the test suite, so that we now regularly run more than 150 tests in CI.