The Alt-Ergo SMT Solver’s results in the SMT-COMP 2019

---

The results of the SMT-COMP 2019 were released a few days ago at the SMT whorkshop during the 22nd SAT conference. We were glad to participate in this competition for the second year in a row, especially as Alt-Ergo now supports the SMT-LIB 2 standard.

Alt-Ergo is an open-source SAT-solver maintained and distributed by OCamlPro and partially funded by R&D projects. If you’re interested, please consider joining the Alt-Ergo User’s Club! Its history goes back in 2006 from early academic researches conducted conjointly at Inria & CNRS “LRI” lab, and the maintenance and development work by OCamlPro since September 2013 (see the past releases).

If you’re curious about OCamlPro’s other activities in Formal Methods, see a happy client’s feedback

SMT-COMP 2018

Our goal last year was to challenge ourselves on the community benchmarks. We wanted to compare Alt-Ergo to state-of-the-art SMT solvers. We thus selected categories close to the “deductive program verification”, as Alt-Ergo is primarily tuned for formulas coming from this application domain. Specifically, we took part in four main tracks categories: ALIA, AUFLIA, AUFLIRA, AUFNIRA. These categories are a combination of theories such as Arrays, Uninterpreted Function and Linear and Non-linear arithmetic over Integers and Reals.

Alt-Ergo’s Results at SMT-COMP 2018

For its first participation in SMT-COMP, Alt-Ergo showed that it was a competitive solver comparing to state of the art solvers such as CVC4, Vampire, VeriT or Z3.

Main Track Categories (number of participants)	Sequential Perfs	Parallel Perfs
ALIA (4)
AUFLIA (4)
AUFLIRA (4)
AUFNIRA (3)

The global results of the competition are available here.

SMT-COMP 2019

Since last year’s competition, we made some improvements on Alt-Ergo, specifically over our data structures and the support of algebraic datatypes (see post).

A few changes can be noted for this year’s competition:

• A distinction between SAT and UNSAT in the scoring scheme allowed us to compete in more categories, as Alt-Ergo doesn’t send back SAT.
• The aim of the 24s Scoring is to reward solvers which solve problems quickly.
• The number of benchmarks in each category has changed. For each category, only the benchmarks which were not proven by every solver last year are used. For example: in the division AUFLIRA, 20011 benchmarks were used last year, of which 1683 remained this year.

Alt-Ergo only competed in the Single Query Track. We selected the same categories as last year and added UF, UFLIA, UFLRA and UFNIA. We also decided to compete over categories supporting algebraic DataTypes to test our newly support of this theory. Alt-Ergo’s expertise is over quantified problems, but we wanted to test our hand in the solver theories over some Quantifier-free categories.

Alt-Ergo’s Results at SMT-COMP 2019

We were proud to see Alt-Ergo performs within a reasonable margin on Quantifier Free problems comparing to other solvers over the UNSAT problems, even though these problems are not our solver’s primary goal. And we were happy with the performance of our solver in Datatype categories, as the support of this theory is new.

For the last categories, Alt-Ergo managed to reproduce last year’s performance, close to CVC4 (2018 and 2019 winner) and Vampire.

Single Query Categories (number of participants)	Sequential	Parallel	Unsat	24s
ALIA (8)
AUFLIA (8)
AUFLIRA (8)
AUFNIRA (5)
UF (8)
UFLIA (8)
UFLRA (8)
UFNIA (8)

This year results are available here. These results do not include Par4 a portfolio solver.

Alt-Ergo is constantly evolving, as well as our support of the SMT-LIB standard. For next year’s participation, we will try to compete in more categories and hope to cover more tracks, such as the UNSAT-Core track.

---

About Alt-Ergo

Alt-Ergo is an Open Source automatic solver of mathematical formulas designed for program verification. Alt-Ergo is very successful for proving formulas generated in the context of deductive program verification. It was originally designed and tuned to be used by the Why3 platform. Its development started in 2006 at the Laboratoire de Recherche en Informatique (LRI - CNRS/Inria) of the Université Paris-Saclay and is maintained, developed and distributed since 2013 by the Formal Methods team at OCamlPro.

This work is made possible through research projects like Décysif, Soprano, BWare, Vocal and LCHIP, as well as support from our Alt-Ergo Users' Club members. If Alt-Ergo has been valuable to you, consider joining the Alt-Ergo Users' Club.