The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
The competition will run on the Star-Exec cluster of machines at The University of Iowa.
The machines have these specifications:
# Starexec stats nodes 0 - 32: Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz (2393 MHZ) 10240 KB Cache 129022 MB main memory # Starexec stats nodes 33 - 192: Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz (2393 MHZ) 10240 KB Cache 258294 MB main memory # Software: OS: Red Hat Enterprise Linux Workstation release 6.3 (Santiago) kernel: 2.6.32-431.1.2.el6.x86_64 glibc: gcc-4.4.6-4.el6.x86_64 glibc-2.12-1.132.el6.i686The machines have 2 processors each and 4 cores per processor. For the competition, only one job-pair will be run on a given machine at a given time, on one processor, with 4 cores available, and the available memory will be capped at 129022MB.
However, please note that we may make software and configuration changes before the competition. As part of setting up the solvers, the solvers will be exercized on a few benchmarks to be sure they run successfully.