Sylvain Conchon

Albin Coquereau

Mohamed Iguernlala

Alain Mebsout

Alt-Ergo

à la diffusion de documents scientifiques de niveau recherche, publiés ou non, émanant des établissements d'enseignement et de recherche français ou étrangers, des laboratoires publics ou privés.

Introduction

Alt-Ergo 2.2 is the last version of the SMT solver developed by Université Paris-Sud and the OCamlPro company. In this paper, we present its architecture and main features. We also focus on a recent work for supporting a conservative polymorphic extension of SMT-LIB 2.

Since its first release in 2006, Alt-Ergo has been mainly designed for discharging proof obligations generated by software development frameworks. In particular, some of its features directly come from the Why/Why3 platforms for deductive program verification (also developed at Université Paris-Sud) which provide a rich specification language based on a polymorphic type system à la ML [START_REF] Filliâtre | One Logic To Use Them All[END_REF].

In order to directly handle proof tasks from this system, Alt-Ergo has a native input language for a polymorphic first-order logic and built-in capabilities to reason about parametric userdefined data-structures. The solver also supports quantifiers reasoning (based on E-matching), the free theory of equality, the theory of (integer and rational) arithmetic, enumerations, record data types and the theory of arrays. Recently, a procedure for the theory of floating-point arithmetic has been integrated. Last but not least, Alt-Ergo integrates a powerful mechanism for reasoning about associative-commutative function symbols.

The native input language of Alt-Ergo is not compliant with the SMT-LIB 2 standard and translating formulas from Alt-Ergo to SMT-LIB 2 (or vice-versa) is not immediate. Besides its extension with polymorphism, this native language diverges from SMT-LIB's by distinguishing terms of type bool from formulas (of type prop). This distinction makes it hard for instance to translate efficiently let-in and if-then-else constructs of the SMT-LIB.

In order to work closely with the SMT community, we have implemented in Alt-Ergo 2.2 a new frontend for a polymorphic conservative extension of the SMT-LIB 2 standard, similar to the one proposed by Bonichon et al. [START_REF] Bonichon | Extending SMT-LIB v2 with λ-Terms and Polymorphism[END_REF]. In this paper, we report on this last release and our first experiments with this new language.

The paper is organized as follows. In Section 2, we give an overview of the general architecture of Alt-Ergo 2.2 and present some of its key features:

• A purely applicative (or functional) implementation in OCaml • A Shostak framework extended with AC completion for equational convex theories • A conservative extension of SMT2 (PSMT2) to support prenex polymorphism à la ML • A CDCL SAT solver tuned for simulating Tableau-like resolution method • A collaborative framework for non-linear arithmetic based on interval calculus • An interactive graphical user interface AltGr-Ergo

In Section 3, we give syntactic and semantic (typing) details about PSMT2. We also report on some issues to plug this new frontend in Alt-Ergo. Section 4 is dedicated to experimental evaluation. We consider benchmarks coming from deductive programs verification platforms and from the SMT-LIB library. We study Alt-Ergo's performances regarding several parameters like the benefit of polymorphism, the consequence of switching from its historical input language to a polymorphic SMT2 syntax, and the impact of using a CDCL solver instead of the Tableaux-like SAT engine. Finally, we discuss some future works in Section 5 and conclude.

General Overview and Key Features of Alt-Ergo 2.2

The general architecture of Alt-Ergo is depicted in Figure 1. Alt-Ergo is written in OCaml. Each module (rounded box in the picture) is implemented in a modular way as a set of (parameterized) modules. Most of the code (except very few parts like the CDCL algorithm and hashconsing used for maximal sharing) is written in a purely applicative programming style. According to our experimental evaluation (see Section 4), the performance loss inherent to functional programming is offset by the simplicity of use (in particular when backtracking) and the robustness offered by persistent data structures. Alt-Ergo provides decision procedures for reasoning in the combination of the following built-in theories: the free theory of equality with uninterpreted symbols, linear arithmetic over integers and rationals, fragments of non-linear arithmetic, polymorphic functional arrays with extensionality, enumerated datatypes, record datatypes, associative and commutative (AC) symbols, floating-point arithmetic [START_REF] Sylvain Conchon | A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT[END_REF], and fixed-size bit-vectors with concatenation and extraction operators. Universal quantifiers are handled using the usual e-matching technique, extended to deal with type variables.

Shostak combination. One of the main modules of Alt-Ergo is the one which implements the equational reasoning for convex theories (equational convex parts of arithmetic, records, enumerations, . . . ). This algorithm, called CC(X), is reminiscent of Shostak combination: it maintains a union-find data-structure modulo a theory X, equipped with a solver and a canonizer, from which maximal information about implied equalities can be directly used for congruence closure [START_REF] Sylvain Conchon | CC(X): Semantic Combination of Congruence Closure with Solvable Theories[END_REF]. This algorithm has been extended to handle associative and commutative user-defined symbols. The resulting combination method, called AC(X) [START_REF] Sylvain Conchon | Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation[END_REF], is obtained by augmenting in a modular way ground AC completion with the canonizer and solver present for the theory X. For instance, the first goal in Figure 2, which involves AC reasoning (symbol u), the free theory of equality (with the uninterpreted symbol f) and integer linear arithmetic, is automatically proved by Alt-Ergo.

Non-linear arithmetic. To reason about non-linear integer arithmetic, Alt-Ergo implements an algorithm which relies on the extension and collaboration of the AC(X) framework and interval calculus to handle NIA axioms in a built-in way [START_REF] Sylvain Conchon | A collaborative framework for nonlinear integer arithmetic reasoning in alt-ergo[END_REF]. An example requiring non-linear arithmetic reasoning is given in Figure 2. To prove such kind of goals, AC(X) is instantiated with linear integer arithmetic (LIA) to handle equalities of LIA and associativity and commutativity properties of non-linear multiplication. The interval calculus component of Alt-Ergo is used, in addition to standard linear operations over inequalities, to propagate bounds of non-linear terms and to suggest case-splits on finite domains. Polymorphism. The historical input language of Alt-Ergo is a first-order logic with some built-in theories and polymorphic data types. Polymorphic types can appear in built-in theories or in user-defined data types. Alt-Ergo has a type discipline à la ML, which means that type variables are implicitly quantified by prenex universal quantifiers. For instance, the third example in Figure 2 defines a polymorphic axiomatization for lists, where the goal formula combines two kinds of polymorphic lists. As explained in Section 3, we recently added a partial support for the SMT-LIB 2 standard, extended with ML-style prenex polymorphism.

Tableaux-like and CDCL procedures. Since its first versions, Alt-Ergo integrates a Tableaux like SAT solver modulo theories implemented in a purely functional programming style. This solver has many advantages in the context of deductive software verification: first, its search is guided by the shape of formulas that are not required to be in CNF form. In addition, it constructs "small" models compared to CDCL approach. For instance, given a formula ϕ = (a ∨ (b ∨ ϕ 1 )) ∧ (¬a ∨ (¬b ∨ ¬ϕ 1 )) where ϕ 1 is a non atomic sub-formula, the CDCL solver will not conclude that the assignment {a → true, b → f alse} is a model for ϕ, contrary to the Tableaux-like approach. Smaller models have two impacts: first, they allow to limit the number of calls to theories solvers (only literals that are true in the model are sent to theories solvers), and second, they help to manage efficiently the set of ground terms used by the E-matching engine to produce new instances from lemmas. Last but not least, the functional coding style of the Tableaux-like solver simplifies memory management of these instances after non chronological backtracking.

Despite its qualities, the Tableaux-like solver suffers from the lack of an efficient Boolean constraints propagation mechanism and a powerful clauses learning technique. As a result, it may have poor performances on SMT problems with complex Boolean structures. To overcome this issue, we recently worked on a new SAT solver that combines the efficiency of a CDCL engine with the nice properties of the Tableaux-like solver (construction of a small Boolean model, interaction with theories and instantiation engine using a small set of literals and terms). Section 4 gives experimental results for a comparison of these two approaches.

Graphical User Interface. To the best of our knowledge, Alt-Ergo is the only SMT solver equipped with a graphical user interface. The GUI allows to observe the triggers computed for each axiom, the number of instances produced per axiom, the time spent in reasoning engines, and the context that have been used to make a proof (if unsat-cores computation is enabled). One can also modify triggers or add instances manually, prune the context once a proof is done, or limit/disable some axioms. More details about AltGr-Ergo can be found in this paper [START_REF] Sylvain Conchon | AltGr-Ergo, a Graphical User Interface for the SMT Solver Alt-Ergo[END_REF].

Towards a Polymorphic SMT2 Extension in Alt-Ergo

In this Section, we discuss some aspects of our conservative extension of SMT2 to support prenex polymorphism à la ML. We show via small examples the modifications made in SMT2 to add parametric polymorphism, we present some typing rules of the extended language and some implementation details, and we discuss the main difficulties we faced when integrating the new frontend in Alt-Ergo.

Conservative extension of SMT2 language with polymorphism

Syntax.

The syntax of the extension is inspired by the "parameters notation" introduced in the SMT-LIB language 2.6 for algebraic datatypes declaration, and is somehow similar to Bonichon et al. [START_REF] Bonichon | Extending SMT-LIB v2 with λ-Terms and Polymorphism[END_REF]. It consists in binding type variables with the "par" construct in some relevant SMT2 commands, and in using the type variables like any other type in the scope of "par". More precisely, we extended six SMT2 commands to obtain a polymorphic extension as shown in the examples of Figure 3 Type-checking. Type-checking PSMT2 files is done using destructive unification. The type system is similar to Why3's [START_REF] Filliâtre | One Logic To Use Them All[END_REF]. Some of the main rules are given in Figure 4. In these rules, a typing environment is a tuple Γ | ∆ in which Γ a map from type symbols (including parameters) to arities, and ∆ is a map from function symbols (and variables) to tuples (par * , type * , type), where par * denotes the (possibly empty) list of type parameters, and type * denotes the (possibly empty) list of arguments types. We will write Γ τ to say that the type τ is well-formed, and write Γ | ∆ e : τ to say that e has type τ in the environment Γ | ∆ . We use the notation Γ | ∆ ---→ cmd Γ | ∆ for the effect that a command cmd has on a configuration Γ | ∆ . We assume that Γ and ∆ are initialized with some builtin type and function symbols, respectively1 . We will distinguish between two kinds of type variables: parameters introduced with the "par" construct (denoted A 1 , . . . , A n ), and unification variables (denoted α 1 , . . . α n ) introduced during type-checking. We will sometimes use the vector notation for a list of elements. Note that, since we use destructive unification, the rules may have side-effects and the order of the premises is sometimes relevant. The first rule updates Γ after a sort declaration. The second (resp. third) one checks if a type or a parameter (resp. a unification variable) is well-formed. The fourth rule updates ∆ with the signature of a function f declared using declare-fun, possibly with type parameters. For an assert command (rule 5), we first add its type parameters, if any, before type-checking

s ∈ Γ n ≥ 0 Γ | ∆ -----------------→ (declare-sort s n) Γ ∪ (s, n) | ∆ sort declaration Γ ui Γ(s) = n Γ (s u1 • • • un)
typing a type or a par Γ α typing a unification var

distinct( A) f ∈ ∆ Γ ∪ (Ai, 0) τi Γ ∪ (Ai, 0) γ Γ | ∆ -------------------------------------------→ (declare-fun f (par (A 1 • • • An) (τ 1 • • • τm) γ)) Γ | ∆ ∪ (f, ( A, τ , γ)) fun. symb. distinct( A) Γ ∪ (Ai, 0) | ∆ e : Bool type-vars(e) ∈ {A1 • • • An} Γ | ∆ (assert (par (A 1 • • • An) e)) : ok assert Γ | ∆ ti : τi ∆(f ) = ( A, µ, ν) |µ| = n σ = {Ai → αi} δ := µ σ γ := ν σ unify(τi, δi) Γ | ∆ (f t1 • • • tn) : γ typing an app/var Γ τx Γ | ∆ ∪ (x, τx) e : Bool Γ | ∆ (forall ((x τx)) e) : Bool ∀ Γ τ Γ | ∆ e : τ unify(τ, τ ) Γ | ∆
(as e τ ) : τ type annot.

Figure 4: Some typing rules of the PSMT2 extension the expression inside the assertion. Then, if e is well typed, we check that the only type variables occurring in e are those bound by par (i.e. all eventual unification variables are substituted).

Typing an application (f t 1 • • • t n ) is more subtle. Once its arguments are type-checked, we retrieve the declaration of f from ∆, and create a fresh signature f : δ → γ. This is done by replacing every type parameter A i with a fresh unification variable α i . Once this is done, we unify every argument type τ i with its corresponding type δ i . If all unifications succeed, we associate the type γ to the application. It is important to note that the α i are physically shared among δ 1 , • • • , δ n , γ to enable destructive unification, and hence the modification of γ while unifying the τ i against the δ i . Type-checking a variable is a particular case of the "application" case. The two latest rules are obvious.

Note that during the unification process, only "unification type variables" are eventually substituted. Type parameters behave likes "monomorphic" type constants and are never altered.

Similarly, the semantics of our PSMT2 language is similar to Why3's (also described in this paper [START_REF] Filliâtre | One Logic To Use Them All[END_REF]).

Implementation and issues

We implemented the PSMT2 extension as a standalone OCaml library, called psmt2-frontend2 . Our work mainly consists in modifying an auto-generated parser3 to support our syntax extension, and in implementing a type-checker that follows the lines of the typing rules given above. The library produces abstract syntax trees (ASTs) after parsing, and provides a type-checker that decorates different (sub-)expressions of a parsed AST with their respective types. It is currently at an early development stage and needs some improvements (support of Bit-vectors, Floating points, incremental mode, . . . ).

In a second step, we plugged the library in Alt-Ergo in order to support the PSMT2 extension. Currently, the integration consists in translating the type-checked AST produced by psmt2-frontend to Alt-Ergo's (parsed) abstract syntax tree. A better solution would be to directly generate a typed AST or advanced hash-consed data-structures. Unfortunately, since triggers are inferred during type-checking, we are obliged to type-check the AST again in Alt-Ergo.

The issue above is actually not the main difficulty we faced when translating psmt2frontend's AST to our solver. Indeed, until recently, Alt-Ergo had a very limited support for let-in and if-then-else (ITE) constructs. Since the solver makes a clear distinction between propositions and Booleans as outlined in Section 2, supporting all forms of ITE expressions4 required non-trivial modifications in Alt-Ergo. More generally, the distinction between terms and formulas, prevents us from using propositions in user-defined function symbols, as shown in the example (<= (f (or A B)) c). We partially addressed this issue by abstracting formulas that occur inside terms with fresh Boolean variables and introducing the abstraction with a let-in. For instance, the example above is lifted to (let ((fresh_b (or A B))) (<= (f fresh_b) c)). This transformation can done during type-checking, which allows us to not modify existing hash-consed data-structures on terms, literals and formulas.

While our solution only slightly differs from Bonichon et al. [START_REF] Bonichon | Extending SMT-LIB v2 with λ-Terms and Polymorphism[END_REF] regarding syntax and typechecking, the two solutions completely diverge when it comes to effectively reason about polymorphism. In fact, they proposed a monomorphization approach while polymorphism is built-in in our instantiation engine. We refer the reader to this paper [START_REF] Bobot | Implementing Polymorphism in SMT solvers[END_REF] for more details about some subtleties of polymorphism, and how it can be handled in an SMT-solver's back-end.

default drivers shipped with Why3 to (optimally) translate the formulas for every considered solver. In a second step, we apply some transformations to the Why3 files (such as axiomatization of bit-vectors, and floating-point arithmetic, which are not supported by all considered SMT solvers). The goal of this step is to be as fair as possible when comparing results of different solvers. Once the transformations applied, we produce benchmarks using three different drivers: (1) a common SMT2 driver that is basically the CVC4's default driver with the previous additional transformations, (2) a modified version of driver 1 that disables0 polymorphism encoding, allowing us to obtain benchmarks in PSMT2 format, (3) a modified version of driver 2 that outputs formulas in Alt-Ergo's native syntax instead of PSMT2. At the end we obtain benchmarks with seven different encoding: default Alt-Ergo, default CVC4, default Z3, default vampire, common SMT2, common PSMT2, and common Alt-Ergo.

We ran Alt-Ergo 2.2.0, CVC4 1.5, Z3 4.6.0, and Vampire 4.2.2 on these benchmarks on the StarExec platform. Time limit was set to 60 seconds and memory limit to 10 GB. We report in the tables below the number of proved formulas (p), the cumulative time (t) taken to prove them, and the percentage (%). For the graphs, x-axes represent the number of unsat answers and y-axes cumulative time in seconds. Note that, we are mainly interested in unsatisfiability (or dually in validity) in the context of program verification. So, "proved" here means "unsat" (or "Valid").

Impact of polymorphism and of the SAT-solver engine. The table and the graph in Figure 5 show the results obtained when running Alt-Ergo on different benchmarks in the common category. We notice that: (1) in general, the CDCL solver competes equally (or is sometimes better) than the Tableaux-like engine regarding the number of proved formulas and resolution time, (2) resolution rate and resolution time are better when using PSMT2, compared to standard SMT format, (3) for some benchmarks (eg. Why3), Alt-Ergo is better on our native polymorphic language compared to PSMT2, (4) for the SPARK benchmark, we notice that there is not a real difference when comparing results on SMT2 and PSMT2 encoding. Indeed, there is not a lot of polymorphism in these benchmarks.

To sum up, Alt-Ergo is better on a polymorphic input syntax, in particular regarding resolution time. In addition, even if the PSMT2 frontend is new and needs some additional improvements, the results we obtain with it are quite close to those we get with the historical native input language. Moreover, the newly added CDCL solver is better than the old Tableaux-like engine. Fair comparison on SMT2 benchmarks. The table and the graph in Figure 6 show the results obtained when running different solvers on the same SMT2 input files. For readability, y-axis is cropped at 25,000 seconds. We remark that Alt-Ergo performs well in general. This was quite surprising for us, knowing that we mainly rely on functional OCaml data-structures and we didn't extensively investigated their improvement. When looking to the table in more details, we notice that CVC4 and Z3 are really fast on some benchmarks. For instance, this is the case on Why3 and SPARK for CVC4, and on SPARK, RCS3 and p9 for Z3. Comparing solvers on files obtained with their default drivers. The table and the graph in Figure 7 show the results obtained when running different solvers on files obtained with their respective drivers shipped with Why3. As expected, all solvers perform better on these benchmarks compared to table of Figure 6. Moreover, Alt-Ergo with CDCL additionally improves its resolution time significantly. Indeed, total resolution time with its default driver is smaller than those of both Figure 5 and Figure 6. We also remark that CVC4 and Z3 are really good on SPARK benchmarks. Actually, these benchmarks heavily involve Ada "Integer range types" that are encoded as bit-vectors for these solvers. Disabling this transformation in the "common SMT2" benchmark seems to have a negative impact on them.

Benchmarks from SMT-LIB

For the evaluation our new front-end, we selected the and AUFNIRA categories from the SMT-LIB library 5 . Their formulas are, to the best of our knowledge, the closest to deductive programs verification. The result6 are given in Figure 8. Overall, although Alt-Ergo (with both a CDCL-based and with a Tableaux-like SAT solver) is behind the other solvers, the gap is not that big. We were actually positively surprised, as we expected worse resolution rate before benchmarking. A more detailed look at AUFLIRA results shows that Alt-Ergo is performing poorly on peter and why sub-directories. A quick analysis revealed that this is mainly due to triggers inference/instantiation, in particular in presence of let-in constructs.

Conclusion and Future Works

We have presented in this paper the last version of the Alt-Ergo SMT solver. One of the main recent work is a frontend for the SMT-LIB 2 format with a non intrusive extension to support prenex polymorphism. The evaluation of Alt-Ergo on a test-suite coming from deductive programs verification showed that our solver is better on polymorphic input formulas, compared to the monomorphized versions of these inputs. Using these benchmarks, and others coming from the SMT-LIB library, we also noticed a gain of performance when switching from our old Tableaux-like SAT solver to a new CDCL-based engine.

In addition to polymorphism, Alt-Ergo is the SMT solver that is equipped with graphical user interface. It is also one of the latest SMT solvers that is (still) using a Shostaklike procedure to combine theories. A modified version of it (called Alt-Ergo-Zero) is used inside the Cubicle model-checker [START_REF] Sylvain Conchon | Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems[END_REF], and the release 0.95.2 has been qualified by Airbus Industrie to be used as a backend for the Caveat platform [START_REF] Baudin | Caveat: a tool for software validation[END_REF].

In the near future, we plan to improve our psmt2-fronted library as well as its integration in Alt-Ergo. Our ultimate plan is to make PSMT2 the default input language of Alt-Ergo. But, before that, we should consider all the engineering issues discussed in Section 3. Moreover, since we now fully support let-in and if-then-else constructs, we should handle them efficiently, and eventually add some pre-processing in the solver. Finally, it would be interesting to see how to map SMT-LIB's floating-point arithmetic to Alt-Ergo's theory.

Figure 1 :

 1 Figure 1: Overview of Alt-Ergo's architecture

(

  *+-example with an AC symbol -+-+-+-+-+-+-+-+*) logic ac u : int, int -> int logic f : int -> int goal g : forall a,c1,c2,e1,e2,d,b : int. (u(a,c2 -c1) = a and b = e2 and u(e1,e2) -f(b) = u(d,d) and d = c1 + 1 and u(b,e1)=f(e2) and c2 = 2 * c1 + 1) -> a = u(a,0) (*+-example with non-linear arithmetic +-+-+-+*) logic v,t : int goal g : forall w, x,y,z: int. v * t = 3 -> v * w = 5 -> -(y*y*y) + 3 * w -5 * t <= -10 -> 0 <= x -> x <= 5 -> 2 * z * ( x / y) + 3 * x = 4 -> 3 * (x / y) * x <= 0 -> false (*+-example with polymorphism +-+-+-+-+-+-+-+-*) type 'a list logic nil : 'a list logic cons : 'a, 'a list -> 'a list logic hd: 'a list -> 'a logic tl: 'a list -> 'a list axiom construction : forall l:'a list. l<> nil -> cons(hd(l),tl(l)) = l axiom hd_cons : forall x:'a. forall l:'a list. hd(cons(x,l)) = x axiom tl_cons : forall x:'a. forall l:'a list. tl(cons(x,l)) = l goal g : forall l:'a list. forall r:('a list) list. r <> nil -> l = hd(r) -> l <> nil -> cons(cons(hd(l),tl(l)), tl(r)) = r

Figure 2 :

 2 Figure 2: Three examples written in Alt-Ergo's native input language

  . Original SMT examples are given on the left, and similar examples with polymorphism on the right.

  (declare-datatype ip ((iP (il Int) (ir Int))))(declare-const x Int) (declare-fun f (Int Int) Int) (assert (forall ((x Int)) (> x 1))) (define-fun foo_f ((x Int)) Real (+ x x)) (define-fun-rec foo_h ((b Int)) Int) (foo_h b)) (define-funs-rec ((foo_u ((a Real) (b Int)) Int) (foo_v ((c Int) (d Real)) Int)) ((foo_v b a) (foo_u d c))) (declare-datatype p (par (A B) ((P (l A) (r B))))) (declare-const y (par (A) A)) (declare-fun g (par (B C) (B C Int) B)) (assert (par (A) (forall ((x A) (y A)) (= x y)))) (define-fun foo_g (par (A B) ((x A)(y B)) B) (g y x 3)) (define-fun-rec foo_i (par (A) ((b A)) A) (foo_i b)) (define-funs-rec ((foo_w (par (X) ((a X) (b Int)) Int)) (foo_x (par (Y) ((c Int) (d Y)) Int))) ((foo_x b a) (foo_w d c)))

Figure 3 :

 3 Figure 3: Modified commands to support polymorphism in SMT2.

Figure 5 :

 5 Figure 5: Comparing Alt-Ergo with different SAT-solvers and on different input languages

Figure 6 :

 6 Figure 6: Comparing Alt-Ergo with other solvers on the same SMT2 input files

Figure 7 :

 7 Figure 7: Comparing solvers on files obtained with their respective drivers

Figure 8 :

 8 Figure 8: Results on AUFLIRA and AUFNIRA: only unsat answers are reported, the % is computed w.r.t. total number of formulas in each directory. X-axes are zoomed in the graphs.

Depending on the logic that has been set with set-logic command.

https://github.com/Coquera/psmt2-frontend

http://homepage.divms.uiowa.edu/~astump/software/ocaml-smt2.zip

Like, for instance, (<= x (ite (A or B) 1 (+ y 2)))

See here http://smtlib.cs.uiowa.edu/logics.shtml for the meaning of these categories.

time limit = 60 seconds, memory limit = 10 GB, only 'unsat' answers are reported.

Acknowledgment. We thank the anonymous reviewers for their remarks which helped us improve this paper. We also thank AdaCore for providing SPARK benchmarks in Why3 format.

This work is partially supported by VOCaL (ANR-15-CE25-0008) and SOPRANO (ANR-14-CE28-0020) ANR projects.

Experimental Evaluation

In this section, we evaluate Alt-Ergo on a set of benchmarks coming from programs verification. We will study Alt-Ergo's performances regarding several parameters like the benefit of polymorphism, the consequence of switching from its historical input language to a polymorphic SMT2 syntax, and the impact of using a CDCL solver instead of the Tableaux-like SAT engine. We also compare Alt-Ergo to some state-of-the-art (SMT) solvers on the benchmarks above, and on benchmarks taken from the SMT-LIB library. All benchmarks, StarExec jobs and detailed results are available here: https://gitlab.com/Coquera/SMT-Workshop--2018.

Benchmarks from program verification

We will consider four sources of benchmarks: SPARK programs from AdaCore's github, C programs taken from Fraunhofer Fokus' ACSL by Example project, Why3's gallery of verified programs, and four industrial B projects that were previously discharged automatically or interactively with Atelier-B. Two of these projects (called DAB and RCS3) were provided by Mitsubishi Electric R&D Centre Europe. Two additional benchmarks (called p4 and p9) were provided by ClearSy. All these benchmarks are translated to Why3. Formulas are then produced in different input formats using Why3's drivers technology [START_REF] Bobot | Why3: Shepherd your herd of provers[END_REF], as shown in Figure above. First, we use the