Alt-Ergo is an SMT solver with strong ties to the deductive program verification framework Why3. It is used by industrial program verification tools such as Frama-C, TIS-Analyzer and SPARK. In this paper, we present recent developments to Alt-Ergo and its frontend, Dolmen. We describe a new bit-vector solver currently under development in Alt-Ergo that supports the arithmetic and logic operators from the SMT-LIB “BV” logic. We also describe the changes made to Dolmen to support version 2.7 of the SMT-LIB standard. Alt-Ergo's new bit-vector solver leverages a new constraint propagation architecture, a rewritten interval module, and standard propagators adapted to Alt-Ergo's Shostak-like combination procedure. We provide some preliminary benchmark results, and report on our experience and ongoing challenges.
Alt-Ergo historically used a purely functional Tableaux-like solver for boolean constraints, which guided most of the design. The Tableaux solver is still present, but Alt-Ergo now includes a CDCL solver with Tableaux-like extensions that is now used as the default solver. The theory modules are shared between both solvers, and combined by a Shostak-like combination procedure. the SMT-LIB v2 standard
Alt-Ergo’s native language Dolmen Parser
API
Dolmen Typer Creation of the hashconsed internal ASTs
Solvers unknown unsat front end back end
One of Alt-Ergo’s central modules is the one implementing equational reasoning for convex theories.
The original algorithm, called CC(X) [
It is also at this level that case splits coming from theories (rather than from boolean disjunctions in the input formula) are handled.
Alt-Ergo supplements the core (“Shostak”) algorithm used to decide equality with theory-specific solvers to deal with the non-equational parts of theories. Each solver is responsible for storing the relevant information in its own module. Theory solvers communicate through equalities (that are processed by the CC(X) algorithm to produce substitutions that are then propagated to all theories) and predicates. Each theory is also able to provide the solver with case-splits to deal with non-convex theories.
Alt-Ergo provides theory modules for linear arithmetic over integers and rationals, fragments of
nonlinear arithmetic, polymorphic functional arrays with extensionality, algebraic data types, associative
and commutative symbols (built into the AC(X) algorithm), floating-point arithmetic [
Non-linear arithmetic Alt-Ergo uses a combination of the AC(X) framework and interval calculus
to handle non-linear integer arithmetic in a built-in way [
ADTs Alt-Ergo supports algebraic data types. This is handled through the native combination of Shostak solvers for the theory of records and of enumerated data types. The theory of enumerated data types, and by extension of records, is not convex, so the Shostak solver is not complete. We supplement the Shostak solver with a relational theory that keeps track of possible constructors and then uses the case split mechanism. Within a case split the Shostak solver for records is used. Floating-point arithmetic Alt-Ergo does not (yet) support the theory of floating-point numbers. Instead, Alt-Ergo supports a theory of a round function which returns the rational closest to a real according to a given floating point specification (bits of exponent, bits of mantissa, and rounding mode).
This theory is currently used by tools such as Why3 by wrapping it in an algebraic data type to represent the extra values (infinites, not-a-number, negative zero). We plan on integrating these wrappers in Alt-Ergo itself to provide direct support for the SMT-LIB theory of floats.
Many theories in Alt-Ergo make use of constraint propagation and store domains on the variables in the problem; however, until recently, each theory solver had its own ad-hoc implementation of domains (intervals for arithmetic, finite sets for enumerated types) and propagators (simplex and additional non-linear propagators for arithmetic, intersection on equality for enumerated types).
In Alt-Ergo 2.6, we introduced a new generic constraint propagation architecture and made it available to theories. Domains are now stored within the same union-find data structure that is used for equational reasoning, while propagators are implemented within each theory’s module.
This new architecture allowed us to simplify the existing experimental theory of algebraic data types and merge it with the existing theories for enumerated data types and records while preserving reasoning power. The constraint-based implementation of arithmetic and logic bit-vector operators, described in Section 3, also uses these new capabilities. The linear arithmetic module is the only remaining module that has not been converted to this new architecture yet.
One limitation of the current implementation is that each theory is responsible for performing its own propagations, restricting opportunities for cross-theory propagations: there is currently no mechanism for notifying a theory when a diferent theory’s domain shrinks. Work is ongoing to integrate constraint propagation into Alt-Ergo’s main equality and predicate processing loop, opening the path to more lfexible scheduling opportunities.
Alt-Ergo supports the SMT-LIB language as input since Alt-Ergo 2.2 [
That means that most of the changes to support SMT-LIB 2.7 (except for bit-vectors), are in the
frontend of Alt-Ergo, where we use the library from the Dolmen project [
Polymorphism Alt-Ergo and Dolmen already support polymorphism, through both Alt-Ergo’s native
language and a polmoyphic extension of SMT-LIB 2.6 [
Higher-order SMT-LIB 2.7 adds maps, which are encodings of higher-order functions in first-order logic. While this can be easily handled by a regular theory that defines an abstract type (for maps) and the function application operator, there is one part of the specification that makes support for higher-order application a bit tricky: the syntax for regular application is overloaded to also represent application of the higher-order application operator. Correctly handling this requires a fair bit of care to properly distinguish the regular first-order applications from the higher-order applications using the first-order syntax, which is also made more complex by the presence of polymorphic maps (i.e., polymorphic functions with no term arguments and that return a map).
We now describe the implementation of the bit-vector theory in Alt-Ergo. The bit-vector theory is implemented by the combination of: • An existing solver for the core bit-vector theory (concatenations and extractions), extended to support negation – not described in this paper; • A constraint propagation mechanism (described in this paper) for other operators, providing full support for the SMT-LIB theory of fixed-size bit-vectors.
The implementation of domains and propagators follows Chihani et al. [
The core bit-vector theory with concat and extract is integrated in the Shostak solver, and was recently
updated to also support negation. While it is possible to further extend the solver to represent arbitrary
bitwise operators as in Cyrluk et al. [
The propagators for bit-vectors rely on two types of domains: bitlists and intervals. These are integrated into the new constraint propagation interface introduced in Alt-Ergo 2.6.
Bitlists Bitlists are domains used to represent the three possible states of bits in a bit-vector: a bit is either set (known to be 1), cleared (known to be 0), or unknown. The concrete representation of bitlists in a computer system is crucial for performance. In Alt-Ergo, we use arbitrary-size integers (provided by the Zarith library, itself using GMP) to represent the domain of as a pair ⟨1, ⟩ where 1 represents the bits known to be set in and represents the bits that are not known in (could be either set or cleared).
The use of big integers to represent bitlists allows very eficient implementations for logical bit-vector
operations, which we adapt from Chihani et al. [
For addition and subtraction, we use the algorithms from Dougall [
The propagator shown in Figure 2 is used for addition (logic operators are extended to bit-vectors by operating independently on each bit). 1 (resp. 1) is a mask of the bits known to be 1 in (resp. ), and is a mask of the bits whose value in (resp. ) is unknown. is the result of the addition when all unknown bits are 0, and is the result when all unknown bits are 1. is a mask of the unknown bits in the result, and 1 is a mask of the bits known to be 1 in the result.
The crucial step is in Equation (3): because the carry in a binary addition is at most one bit, overflow is only possible on the bits where and disagree, which are added to the unknown bits of and .
We do not implement precise propagators for multiplication as that would have a quadratic complexity. Instead, we simply compute the known low bits (efectively providing an implementation of congruence modulo powers of two), and rely on case splits or other integer reasoning to deal with multiplication. 1 = ∧ ¬ smallest (unsigned) result largest (unsigned) result overflow is possible where and disagree bits set in both and are set if known
Although the SMT-LIB bit-vector theory uses bit-vectors with a specific (parametric) width, our bitlists do not encode the width explicitly, relying on the types to encode this information instead. Intervals Alt-Ergo already included a module to represent union of intervals, with explanations (justifications) for each of the gaps between intervals. However, this module was found to be hard to extend to properly support bit-vector operations, notably concatenation and extraction. We rewrote the interval module with a parametric implementation providing basic building blocks to manipulate intervals while correctly preserving explanations. Preserving correct explanations is critical for the soundness of the whole solver, and isolating the code that needs to deal with them makes the code easier to reason about and maintain. Those basic building blocks are then used to safely lift high-level operations such as addition, multiplication, and extraction from intervals to unions of intervals. This new interval module is now used for both the bit-vector solver and the arithmetic solver, although we do not yet have direct communication between the intervals stored by both solvers (see Section 2.3).
Note that using union of intervals (rather than just intervals) allows representing precisely intervals for bit-vectors, without loss of precision in case of overflows or underflows. Instead, we simply implement an operator (using the API described below) to implement an extract function that returns the low bits of an interval. For instance, when using 8-bit arithmetic, subtracting 4 from the interval [0, 241] yields [− 4, 237]; we then call extract for the low bits of this interval to obtain the union [0, 237] ∪ [251, 255].
The use of unions in the representation is relatively controlled. In particular, we do not create holes
in the union from information coming from the (low) bits of a variable. For instance, if is an 8-bit
variable that is known to have its least-significant bit set, its interval is obtained by doubling [0, 127]
then adding 1, and so is [
Ordered Types The interval module is parametric over an ordered type. An ordered type extends a type of “finite values” (typically integers or rationals) with a positive and negative innfiites, and also provide a successor and a predecessor funtion.
The successor and predecessor functions do not exist on rationals: we use the well-known trick of infinitesimals, i.e., we use pairs + where is a rational, is an integer, and is an infinitesimal considered smaller than any rational.
This allows the representation of open rational intervals such as (3.5, 7) by closed intervals such as [3.5 + , 7 − ]. In practice, infinitesimals are not exposed by the ordered type interface, and the rest of the interval module only makes use of a few documented axioms (e.g., pred(succ()) = if is finite) on the predecessor and successor functions, providing flexibility in the actual implementation of the ordered type interface.
Core Intervals The core of the interval module is a functor taking an ordered type and returning a “core interval” module. We use two representations of intervals: a normalized representation, with type union (represented as a sequence of disjoint intervals with an explanation for the gaps) and an unnormalized one, with type set (represented as an arbitrary set of intervals). Intervals are stored in the normalized representation, but the unnormalized representation can be used to implement complex operations.
The core interval API exposes higher order functions to convert from operations on intervals or bounds without explanations to core intervals (union and set types) with explanations. Some examples of such functions include: • The function map_to_set computes the image of an union by an arbitrary isotone function f over intervals, i.e., a function monotone with respect to inclusion (if 1 ⊆ 2 then (1) ⊆ (2)). • The function partial_map_inc computes the image of a partial increasing function such as the conversion from reals to integers. • The function trisection_map_to_set is provided to split a union between the values strictly smaller than a central value , the singleton {} (if within the union) and the values strictly larger than . This is used to provide piecewise definitions of multiplication, division. Interval Algebra The rest of the interval module is concerned with lifting arithmetic operations from values to intervals, using the functions provided by the core interval module. Crucially, this does not need to care about explanations: implementers only need to make sure to use the appropriate function from the core interval module (depending on e.g., monotony of the implemented function). This principled design makes the code for interval operations clearer and easier to read, as it is not interleaved with concerns about explanations. The design made it possible to implement the new functions related to euclidean division that were required for bit-vector operations with reasonable confidence. This also allowed us to improve the precision of explanations in the implementation of multiplication: the existing implementation used coarser explanations than necessary out of an abundance of caution, but the generic implementation of monotone functions in the core interval module is able to preserve more precise explanations.
Propagators are registered on specific domains of the variables. When the corresponding domain is reduced and changes, all the propagators that are watching this specific domain fire and add added to a queue for further propagation. Depending on the constraint, propagators are registered either only on the bitlist domains (this is the case for bit-wise operators such as bvor or bvand), only on the interval domains (this is the case for division and remainder), or both bitlist and interval domains.
In addition, special “cross-domain” propagators are used to perform reductions between the bitlist
and interval domains. These are taken from Chihani et al. [
We currently use a simple scheduling strategy, repeated until a fixpoint is reached: first we saturate same-domain propagators separately for each domain, then we saturate cross-domain propagators.
The bit-vector module is integrated into the case-split mechanism for completeness and model generation. We perform case splits on bit-vectors by selecting a value for the most significant unknown bit from one of the variables in the problem with minimal, non-fully-known, domain size. This is the simplest heuristic that we found to perform reasonably well.
The use of case splits for bit-vectors revealed that the current implementation in Alt-Ergo is too
aggressive, and Alt-Ergo can end up spending a lot of time performing unnecessary bit-vector case
splits when making a single boolean decision would allow to conclude quickly. Currently, control
does not return to the outer CDCL solver until a satisfying bit-vector assignment has been found. We
plan on tackling this issue by better integrating the case split mechanism with the outer CDCL solver,
and exploring strategies for selecting case splits along the lines of the labelling strategies described in
Chihani et al. [
Alt-Ergo uses a simplex algorithm for linear arithmetic, but does not have a solver for diference logic.
Chihani et al. [
We implemented an incremental solver for diference logic following Feydy et al. [
The diference logic solver is still experimental and has not been integrated into the main development branch of Alt-Ergo yet. It has not been used for the benchmarks in the experimental evaluation section.
In order to leverage the simplex algorithm for integer variables, and to better handle conversions between bit-vectors and integers (either using the non-standard bv2nat and int2bv functions, or the new conversion operators from the SMT-LIB standard version 2.7), we maintain two maps between canonical representatives of bit-vector and integer variables.
Note that theory solvers in Alt-Ergo are mostly independent; hence, we alternate between runs of the constraint propagation described in this paper and runs of the simplex algorithm for pure integer problems. We plan on later improving the integration of the simplex into the constraint propagation mechanism.
This conversion is currently only performed for bit-vector expressions that appear within a bv2nat
constructor, or within a (bit-vector) comparison such as bvule, bvult, etc. We are interested in
investigating whether performing this conversion for all bit-vector terms, as in int-blasting [
Map from bit-vectors to integers For a bit-vector variable , we maintain a map from all the right-shifts of (defined below) to a corresponding integer variable. If has type (_ BitVec w), i.e., a bit-vector of width , we create an integer constant to represent the integer value of the extraction of bits , + 1, ..., − 1 of (using a little-endian convention, so bit − 1 is the most significant bit). If we denote bv2nat() the value of a bit-vector as an integer (as defined in the SMT-LIB specification), the value bv2nat() is also equal to ⌊bv2nat()/2⌋, i.e., the right arithmetic shift of bv2nat() by . Appropriate inequalities to encode this (floored) division are also added to the simplex.
For an extraction [,] of bits , + 1, ..., − 1, we then compute bv2nat([,]) as − 2− . Concatenations are similarly represented by multiplying by the appropriate power of 2.
Using right-shift in this way allows to limit the number of integer variables created to represent extractions to be linear (rather than quadratic) in the bit-vector width.
This map is updated when the canonical representative of a bit-vector equivalence class changes, propagating relevant information on the integer variables for consumption by the simplex. Map from integers to bit-vectors Integer variables are represented in Alt-Ergo’s Shostak solver by a polynomial. We maintain a similar map from polynomials to the corresponding bit-vector variable, which may have been introduced to represent a right-shift.
When the canonical representative of an integer variable changes, updating the map allows to propagate new equalities learned by the simplex (in the integers) to corresponding equalities in the bit-vectors, which can cause further propagations on bit-vector domains.
Conversion of bit-vector arithmetic operators Furthermore, we also convert arithmetic expressions on bit-vectors (in the same context as previously, either in bv2nat operations or bit-vector comparisons) into arithmetic expressions on the corresponding integer variables. Unlike int-blasting approaches, we only convert arithmetic operation, not bitwise operations.
For a bit-vector polynomial (using e.g., bvadd, bvmul, etc.) we keep a canonical version with coeficients computed modulo 2 (where is the bit-width). For each distinct bit-vector with the same canonical polynomial we also have a constant defined so that bv2nat() = + 2 (where is the canonical polynomial of and is the bit-width of ). We also record appropriate bounds for bv2nat().
When there is a relation between bit-vectors (e.g., an equality or a comparison), we replicate the relation on the integer variables using the stored polynomial and ofset, which is then picked up by the simplex.
Note that this design is quite diferent from that in Chihani et al. [
In this section, we evaluate Alt-Ergo’s bit-vector capabilities on a set of benchmarks coming from program verification, on a subset of the SMT-LIB QF_BV benchmarks, and on some manually crafted examples. Note that on these benchmarks our implementation still sufers from the “agressive case splits” problem described in Section 3.4 and locks us into a naive strategy. We expect further improvements from re-architecting around the issue.
All the benchmarks below use a time limit of 20 seconds. We only report unsat results.
QF_BV subset We first compare the new solver against other solvers on a random subset of 10498
problems from the QF_BV category of the SMT-LIB benchmarks library [
The QF_BV category only contains quantifier-free bit-vector problems. It is a good proxy to evaluate the strength of the ground bit-vector solver in isolation, but does not necessarily presume of the performance of real-world usage for more complex program verification tasks typically involving quantifiers and multiple theories.
We compare Alt-Ergo with the bit-vector solver against Z3 4.14.1 [
The new solver’s performance is slightly below that of COLIBRI, which is expected – while Alt-Ergo’s
new solver is inspired by the one in COLIBRI, some architectural constraints in Alt-Ergo prevents us
from implementing some crucial reasoning steps. Bitwuzla dominates the competition, especially in
terms of unique problems solved, but does not support the same range of theories as the other solvers.
Benchmarks from program verification Since Alt-Ergo is frequently used within the Why3
toolchain, it is relevant to compare the performance of the new solver against other solvers using this
toolchain. We now focus on an internal benchmark set of 9,038 industrial problems provided by one of
our partners in the DéCySif project. These problems have been generated from verification conditions
of C programs using the J3 tool. They are translated into SMT-LIB by Why3 [
Unlike the QF_BV category of SMT-LIB benchmarks that only compares the ground bit-vector solvers, this benchmark set provides a more contextual comparison. The problems involve bit-vectors and other SMT features such as uninterpreted functions, uninterpreted sorts, floats and integers and are more representative of real-world program verification workflows.
For Alt-Ergo, two diferent drivers are used: a legacy driver using a Why3-provided axiomatization of bit-vectors, and a new driver using the SMT-LIB BV primitives developed in this work (shown as “Alt-Ergo + BV” in the tables).
We compare the performance of solvers on the J3 dataset in Table 2. The “Alt-Ergo (ax)” solver is the development version of Alt-Ergo without the new bit-vector solver, and instead uses the Why3 axiomatization. The “Alt-Ergo + BV” solver is the new bit-vector solver described in this paper. The table shows that the new bit-vector solver provides a significant improvement to Alt-Ergo’s reasoning abilities on this dataset. We also compare the performance of Z3 4.14.1 and CVC5 1.2.1 on this benchmark set. We did not take Bitwuzla and Yices on because they do not support all the theories used in these benchmarks: Bitwuzla does not support uninterpreted sorts and Yices does not support FP theory. We are not retaining results for COLIBRI because it encountered errors on most of these files. The unique column provides the number of benchmarks that are only solved by a specific solver. In wtime unsat column, we focused on the subset of 5,335 problems solved as unsatisfiable by all solvers in Table 2. The wtime unsat is the wall time (in seconds) spent by the solver over this specific subset.
The new solver solves more problems than Z3. It also solves less problems than CVC5 overall, but is still able to provide a reasonable contribution in terms of unique results, providing complementarity. Manually crafted examples Finally, we examine the behavior of diferent solvers on some simple problems with bit-vector-to-int conversions. We compare Alt-Ergo (with the bit-vector solver) to Z3 4.13.4 and CVC5. Note that we use the non-standard bv2nat rather than the new ubv_to_int function from SMT-LIB 2.7 as ubv_to_int is not supported by all solvers.
The first two examples, shown in Figure 3, state a simple property relating the conversion to integers of the low and high bits of a bit-vector of width 64. These examples illustrate a strength of integration with the existing core bit-vector solver and the Shostak combination procedure in Alt-Ergo: while Z3 is able to quickly prove the first example with concat, it fails to do so when using the logically equivalent formulation using extract. On the other hand, the Shostak-based solver in Alt-Ergo efectively normalizes the second example to the first, and Alt-Ergo is able to prove both. (declare-const x (_ BitVec 64)) (declare-const hi (_ BitVec 32)) (declare-const lo (_ BitVec 32)) (assert (not (=> (= x (concat hi lo)) (= (bv2nat x) (+ (* 4294967296 (bv2nat hi))
(bv2nat lo)))))) (check-sat)
The last example, shown in Figure 4, is another simple property regarding the absence of overflow of integers when computing a bit-vector addition. As the bvuaddo operator from SMT-LIB 2.7 (used to detect when an addition overflows) is not supported by all solvers, we use a straightforward encoding using bv2nat instead using the standard’s definition of the operator. This simple example is only proved by Alt-Ergo thanks to the communication between the integer and bit-vector theories.
The results on the handcrafted examples are summarised in Table 3.
We have presented in this paper recent developments in the Alt-Ergo SMT solver. The main improvements are support for arithmetic and logical bit-vector operators from the SMT-LIB theory “BV”, and the support for the SMT-LIB standard version 2.7 through Dolmen.
The implementation of arithmetic and logical bit-vector operators follows closely Chihani et al. [
In the near future, we plan to improve direct cross-theory propagations (notably between bit-vectors
and arithmetic), and integrate the diference logic solver (called the global Delta domain in Chihani
et al. [
During the preparation of this work, the authors used Gemini 2.5 in order to: Peer review simulation. Further, the authors used ChatGPT for the abstract in order to: Improve writing style. After using this tool, the authors reviewed and edited the content as needed and take full responsibility for the publication’s content.