SMT-LIB community has been contributing benchmarks and holding competitions for several years. They can be considered as good standard benchmarks for SMT solvers. We have select integers, bit-vectors, and quantifiers related benchmarks for our tests. These tests are within QF-IDL, QF-NIA, QF-UFBV, QF-UFLIA, UFNIA, QF-BV, QF-LIA, QF-UF, QF-UFIDL.
We also select the Bounded Model Checking and k-induction problems within QF-LIA benchmarks from 2012 SMT Competition to test their abilities of applying inductive axioms.
All of the benchmarks are in the SMT-LIB 2.0 format, most of which should be handled by both solvers. But in practice, Alt-Ergo reports typing error and parsing error on some test inputs because its current version 0.95.1 does not fully support it yet. And also, some of the benchmarks do not indicate expected results. They are either unknown or not available at all. Therefore, we only considered those can be handled by both solvers, and had an expected answer of sat/unsat as valid benchmarks when we were analysing the result.
We wrote a testing script to run the tests. The script first randomly selected test inputs from all the benchmarks. Secondly, both solvers were invoked for each input, individually, not simultaneously. Thirdly, their execution time was captured by Unix time utility, and the real wall time was considered as their execution time. Finally, there was a timeout of 30 seconds. If any of them reached 30 seconds, it was killed.
Since Alt-Ergo cannot handle inputs with an expected answer of sat, we just skipped that for Alt-Ergo, and only use that input as a measure of efficiency/capability for CVC4 only.
For BMC and k-induction problems, we had a different strategy. Each of those benchmarks consists of multiple smaller problems, which require the solver to solve them incrementally. Therefore we set up a timeout of 15 seconds, to compare how much problems they can solve in a limited time.
We ran the tests on a Core i5-3320M 2.6GHz dual core CPU with 8GB memory, on Ubuntu 13.04 32bit operating system. During testing, no other job is allowed.