This site allows you to browse the SMT-LIB benchmarks. Select a logic or family below to see the benchmarks in this family. The benchmark pages show benchmark metadata and historic competition results. There is also a page with informative charts for each logic, and a comparison of the solvers on the logic. See the chart pages for an explanation.
The SMT-LIB benchmarks can be downloaded from Zenodo (non-incremental, incremental). The database that was used to generate this website is also available on Zenodo.
| QF_ABV • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| calc2 | 2010-07-15 | |
| Wolf-fmbench | 2019-01-01 | 2019-07-07 |
| btfnt | 2010-07-15 | |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| ecc | 2014-07-21 | |
| sharing-is-caring | 2014-07-21 | |
| dwp_formulas | 2011-06-30 | |
| stp | 2007-07-03 | |
| jager | 2013-07-02 | |
| platania | 2007-07-03 | |
| bench_ab | 2006-08-21 | |
| pipe | 2010-07-15 | |
| brummayerbiere | 2008-07-07 | |
| brummayerbiere2 | 2008-07-07 | |
| egt | 2006-08-21 | |
| Yurichev | 2020-04-15 | 2020-07-06 |
| stp_samples | 2011-06-30 | |
| klee-selected-smt2 | 2014-07-21 | |
| bmc-arrays | 2014-07-21 | |
| brummayerbiere3 | 2009-08-02 | |
| Mann | 2018-01-01 | 2018-07-14 |
| Mann | 2019-01-01 | 2019-07-07 |
| Wolf-fmbench | 2018-01-01 | |
| CPAchecker_kInduction-SoSy_Lab | 2019-03-07 |
| QF_ABVFP • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Heizmann-UltimateAutomizer | 2017-05-01 | 2017-07-23 |
| Vector | 2021-02-11 | 2021-07-18 |
| Liew-KLEE | 2017-04-28 | 2017-07-23 |
| CPAchecker_kInduction-SoSy_Lab | 2019-03-07 |
| QF_ABVFPLRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| Heizmann-UltimateAutomizer | 2017-05-01 | 2017-07-23 |
| QF_ALIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| ios | 2006-08-21 | |
| qlock2 | 2006-08-21 | |
| array_benchmarks | 2005-07-12 | |
| piVC | 2006-08-21 | |
| cvc | 2005-07-12 | |
| UltimateBuchiAutomizer |
| QF_ANIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| AutomizerLoopAcceleration | 2024-04-13 | 2024-07-22 |
| UltimateAutomizer | 2015-07-02 | |
| GrandProduct-Ozdemir | 2021-12-13 | 2022-08-10 |
| UltimateAutomizer2 | 2016-07-02 | |
| UltimateBuchiAutomizer |
| QF_AUFBV • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Wolf-fmbench | 2019-01-01 | 2019-07-07 |
| Alive2 | 2021-03-01 | 2021-07-18 |
| Gonzalvez | 2019-01-01 | 2020-07-06 |
| Alive2-partial-undef | 2021-03-01 | 2021-07-18 |
| ecc | 2014-07-21 | |
| nysm | 2023-10-02 | 2024-07-22 |
| Wolf-fmbench | 2018-01-01 | |
| CPAchecker_kInduction-SoSy_Lab | 2019-03-07 |
| QF_AUFBVFP • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Alive2 | 2021-03-01 | 2021-07-18 |
| QF_AUFBVLIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| CPAchecker_kInduction-SoSy_Lab | 2019-03-07 |
| QF_AUFBVNIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| CPAchecker_kInduction-SoSy_Lab | 2019-03-07 |
| QF_AUFLIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Rodin | 2017-08-29 | 2019-07-07 |
| check | 2005-07-12 | |
| array_benchmarks | 2005-07-12 | |
| cvc | 2005-07-12 | |
| swap | 2007-07-03 | |
| storecomm | 2006-08-21 | |
| storeinv | 2007-07-03 | |
| ultimateKojak | ||
| ultimateAutomizer | ||
| safari |
| QF_AUFNIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizer | 2015-07-02 |
| QF_AX • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| cvc | 2005-07-12 | |
| swap | 2007-07-03 | |
| storecomm | 2006-08-21 | |
| storeinv | 2007-07-03 |
| QF_BV • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Wolf-fmbench | 2019-01-01 | 2019-07-07 |
| Goel-hwbench | 2018-01-01 | 2018-07-14 |
| Bouvier | 2021-03-12 | 2021-07-18 |
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| Heizmann-UltimateAutomizer | 2017-05-01 | 2017-07-23 |
| ecc | 2014-07-21 | |
| dwp_formulas | 2011-06-30 | |
| stp | 2007-07-03 | |
| bench_ab | 2006-08-21 | |
| pipe | 2010-07-15 | |
| brummayerbiere | 2008-07-07 | |
| brummayerbiere2 | 2008-07-07 | |
| Yurichev | 2020-04-15 | 2020-07-06 |
| stp_samples | 2011-06-30 | |
| brummayerbiere3 | 2009-08-02 | |
| Mann | 2018-01-01 | 2018-07-14 |
| asp | 2011-06-30 | |
| calypto | 2009-08-02 | |
| mcm | 2013-07-02 | |
| Mann | 2019-01-01 | 2019-07-07 |
| uclid | 2005-07-12 | |
| RWS | 2014-07-21 | |
| fft | 2014-07-21 | |
| check2 | 2011-06-30 | |
| pspace | 2014-07-21 | |
| challenge | 2014-07-21 | |
| sage | 2009-08-02 | |
| bruttomesso | 2009-08-02 | |
| MCMPC | 2022-10-12 | 2023-07-06 |
| crafted | 2006-08-21 | |
| gulwani-pldi08 | 2013-07-02 | |
| p4dfa-XiaoqiChen | 2022-12-14 | 2023-07-06 |
| float | 2014-07-21 | |
| tacas07 | 2007-07-03 | |
| wienand-cav2008 | 2009-08-02 | |
| galois | 2013-07-02 | |
| uum | 2011-07-14 | |
| rubik | 2011-06-30 | |
| oisc-gurtner | 2023-02-21 | 2023-07-06 |
| uclid_contrib_smtcomp09 | 2009-08-02 | |
| bv-term-small-rw-Noetzli | 2019-03-11 | 2019-07-07 |
| spear | 2007-07-03 | |
| brummayerbiere4 | 2013-07-02 | |
| grsbits-truby | 2023-02-24 | 2023-07-06 |
| VS3 | 2009-08-02 | |
| bmc-bv | 2014-07-21 | |
| log-slicing | 2014-07-21 | |
| Sydr | 2021-02-19 | 2021-07-18 |
| Weber | 2020-01-01 | 2021-07-18 |
| bmc-bv-svcomp14 | 2014-07-21 | |
| ecrw | 2022-03-15 | 2022-08-10 |
| Sage2 | 2015-07-02 | |
| BuchwaldFried | 2017-01-01 | 2017-07-23 |
| Favaro | 2020-03-28 | 2021-07-18 |
| Hansen-Check | 2017-05-31 | 2017-07-23 |
| Wolf-fmbench | 2018-01-01 | |
| CPAchecker_kInduction-SoSy_Lab | 2019-03-07 | |
| kratos_systemC_swmc | ||
| Coffin | 2021-01-10 | |
| BMC_WMM | 2025-03-15 |
| QF_BVFP • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| Heizmann-UltimateAutomizer | 2017-05-01 | 2017-07-23 |
| schanda | 2015-07-02 | |
| ramalho | 2017-07-23 | |
| Vector | 2021-02-11 | 2021-07-18 |
| Alive2 | 2021-03-01 | 2021-07-18 |
| Liew-KLEE | 2017-04-28 | 2017-07-23 |
| CPAchecker_kInduction-SoSy_Lab | 2019-03-07 |
| QF_BVFPLRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| Heizmann-UltimateAutomizer | 2017-05-01 | 2017-07-23 |
| schanda | 2015-07-02 | |
| Gudemann | 2019-01-01 | 2020-07-06 |
| QF_BVLRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| mapf_r | 2024-04-14 |
| QF_DT • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Bouvier | 2021-03-12 | 2021-07-18 |
| 20172804-Barrett | 2017-07-23 | |
| blocksworld | 2023-07-20 | 2024-07-22 |
| QF_FP • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| Heizmann-UltimateAutomizer | 2017-05-01 | 2017-07-23 |
| wintersteiger | 2015-07-02 | |
| griggio | 2017-07-23 | |
| schanda | 2015-07-02 | |
| ramalho | 2017-07-23 | |
| Vector | 2021-02-11 | 2021-07-18 |
| QF_FPLRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| Heizmann-UltimateAutomizer | 2017-05-01 | 2017-07-23 |
| schanda | 2015-07-02 | |
| Gudemann | 2019-01-01 | 2020-07-06 |
| QF_IDL • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Bouvier | 2021-03-12 | 2021-07-18 |
| sal | 2005-07-12 | |
| check | 2005-07-12 | |
| Averest | 2006-08-21 | |
| mathsat | 2005-07-12 | |
| fuzzy-matrix | 2014-07-21 | |
| RVpredict-BohanLi | 2022-02-14 | 2022-08-10 |
| planning | 2006-08-21 | |
| cellar | 2007-07-03 | |
| DTP | 2005-07-12 | |
| parity | 2008-07-07 | |
| job_shop | 2006-08-21 | |
| jobshop-BohanLi | 2022-02-14 | 2022-08-10 |
| queens_bench | 2006-08-21 | |
| qlock | 2006-08-21 | |
| sep | 2005-07-12 | |
| schedulingIDL | 2008-07-07 | |
| diamonds | 2005-07-12 | |
| RTCL | 2005-07-12 | |
| bcnscheduling | 2008-07-07 | |
| asp | 2011-06-30 |
| QF_LIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| ezsmt | 2019-01-01 | 2021-07-18 |
| tropical-matrix | 2015-07-02 | |
| check | 2005-07-12 | |
| Averest | 2006-08-21 | |
| mathsat | 2005-07-12 | |
| RTCL | 2005-07-12 | |
| Dartagnan | 2021-02-19 | 2021-07-18 |
| calypto | 2009-08-02 | |
| slacks | 2011-06-30 | |
| cut_lemmas | 2010-07-15 | |
| nec-smt | 2008-07-07 | |
| c_inference | 2023-11-17 | 2024-07-22 |
| rings_preprocessed | 2010-07-15 | |
| SMPT | 2022-03-07 | 2022-08-10 |
| rings | 2008-07-07 | |
| prime-cone | 2011-06-30 | |
| pidgeons | 2013-07-02 | |
| CAV_2009_benchmarks | 2010-07-15 | |
| pb2010 | 2011-06-30 | |
| bofill-scheduling | 2009-08-02 | |
| cmodelsdiff | 2019-01-01 | 2021-07-18 |
| tightrhombus | 2014-07-21 | |
| RWS | 2014-07-21 | |
| CIRC | 2005-07-12 | |
| arctic-matrix | 2015-07-02 | |
| convert | 2010-07-15 | |
| dillig | 2013-07-02 | |
| wisa | 2005-07-12 | |
| fft | 2014-07-21 | |
| miplib2003 | 2013-07-02 | |
| Bromberger | 2018-03-26 | 2018-07-14 |
| UltimateBuchiAutomizer | ||
| ultimateKojak | ||
| ultimateAutomizer | ||
| lustre | ||
| kratos_systemC_swmc |
| QF_LIRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| LCTES | 2015-07-02 |
| QF_LRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| tta_startup | 2006-08-21 | |
| ezsmt | 2019-01-01 | 2021-07-18 |
| sc | 2006-08-21 | |
| LassoRanker | 2014-07-21 | |
| clock_synchro | 2006-08-21 | |
| Heizmann-UltimateInvariantSynthesis | 2017-01-01 | 2017-07-23 |
| uart | 2006-08-21 | |
| DTP-Scheduling | 2011-06-30 | |
| keymaera | 2014-07-21 | |
| meti-tarski | 2014-07-21 | |
| sal | 2005-07-12 | |
| tropical-matrix | 2015-07-02 | |
| TM | 2005-07-12 | |
| spider_benchmarks | 2005-07-12 | |
| latendresse | 2014-07-21 | |
| miplib | 2008-07-07 | |
| check | 2005-07-12 | |
| hybrid_networks |
| QF_NIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| ezsmt | 2019-01-01 | 2021-07-18 |
| LassoRanker | 2014-07-21 | |
| sqrtmodinv-hoenicke | 2023-03-28 | 2023-07-06 |
| UltimateAutomizer | 2015-07-02 | |
| LCTES | 2015-07-02 | |
| leipzig | 2009-08-02 | |
| Dartagnan | 2021-02-19 | 2021-07-18 |
| calypto | 2009-08-02 | |
| UltimateLassoRanker | 2015-07-02 | |
| elster | 2025-03-31 | 2025-08-11 |
| mcm | 2013-07-02 | |
| AProVE | 2014-07-21 | |
| MathProblems | 2022-03-15 | 2022-08-10 |
| VeryMax | 2017-04-27 | 2017-07-23 |
| BohanLi | 2025-03-18 | |
| UltimateLTLAutomizer | ||
| AllegroDVT | 2023-03-13 |
| QF_NIRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizer | 2015-07-02 | |
| LCTES | 2015-07-02 |
| QF_NRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| ezsmt | 2019-01-01 | 2021-07-18 |
| LassoRanker | 2014-07-21 | |
| meti-tarski | 2014-07-21 | |
| UltimateAutomizer | 2015-07-02 | |
| Pine | 2020-09-11 | 2021-07-18 |
| Uncu | 2022-03-14 | 2022-08-10 |
| hong | 2014-07-21 | |
| hycomp | 2014-07-21 | |
| Heizmann-UltimateInvariantSynthesis | 2017-05-01 | 2017-07-23 |
| Economics-Mulligan | 2018-05-01 | 2018-07-14 |
| pPDA-Chiari-Pontiggia-Winkler | 2024-04-07 | 2024-07-22 |
| Sturm-MBO | 2016-11-05 | 2017-07-23 |
| Geogebra | 2021-11-01 | 2022-08-10 |
| Sturm-MGC | 2016-11-05 | 2017-07-23 |
| kissing | 2014-07-21 | |
| zankl | 2010-07-15 |
| QF_RDL • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| sal | 2005-07-12 | |
| check | 2005-07-12 | |
| SMT-Temporal-Planning-Benchmarks | 2013-07-02 | |
| scheduling | 2005-07-12 | |
| skdmxa | 2005-07-12 | |
| skdmxa2 | 2006-08-21 |
| QF_S • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| omark | 2024-03-18 | 2024-07-22 |
| rna | 2025-04-03 | 2025-08-11 |
| woorpje-lu | 2023-03-29 | 2023-07-06 |
| pcp-string | 2025-04-03 | 2025-08-11 |
| negated-predicates | 2025-04-11 | 2025-08-11 |
| matching | 2025-04-10 | 2025-08-11 |
| automatark-lu | 2023-03-29 | 2023-07-06 |
| Jiang | 2019-01-01 | 2020-07-06 |
| hornstr-equiv | 2025-04-11 | 2025-08-11 |
| sygus-qgen | 2020-01-01 | 2020-07-06 |
| hornstr | 2025-04-11 |
| QF_SLIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| woorpje-lu | 2023-03-29 | 2023-07-06 |
| matching | 2025-04-10 | 2025-08-11 |
| Jiang | 2019-01-01 | 2020-07-06 |
| Norn | 2015-01-01 | 2020-07-06 |
| transducer-plus | 2023-03-31 | 2023-07-06 |
| stringfuzz-lu | 2023-03-27 | 2023-07-06 |
| redos_attack_detection | 2024-04-11 | 2024-07-22 |
| str-small-rw-Noetzli | 2019-03-11 | 2020-07-06 |
| webapp | 2023-04-03 | 2023-07-06 |
| Reynolds | 2018-05-23 | 2018-07-14 |
| full_str_int | 2019-01-01 | 2020-07-06 |
| Leetcode | 2019-01-01 | 2020-07-06 |
| Kepler | 2018-01-01 | 2020-07-06 |
| denghang | 2023-03-29 | 2023-07-06 |
| QF_SNIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| elster | 2025-03-31 | 2025-08-11 |
| Reynolds | 2018-05-23 | 2018-07-14 |
| Wu-PyExZ3 | 2020-02-24 | 2021-07-18 |
| QF_UF • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Rodin | 2017-08-29 | 2019-07-07 |
| Goel-hwbench | 2018-01-01 | 2018-07-14 |
| CLEARSY | 2019-09-06 | 2020-07-06 |
| eq_diamond | 2008-07-07 | |
| TypeSafe | 2014-07-21 | |
| NEQ | 2005-07-12 | |
| QG-classification | 2007-07-03 | |
| SEQ | 2005-07-12 | |
| PEQ | 2005-07-12 |
| QF_UFBV • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| calc2 | 2010-07-15 | |
| Wolf-fmbench | 2019-01-01 | 2019-07-07 |
| Goel-hwbench | 2018-01-01 | 2018-07-14 |
| Bouvier | 2021-03-12 | 2021-07-18 |
| Jaroslav-Bendik-Certora | 2023-03-14 | 2023-07-06 |
| Certora | 2024-11-13 | 2025-08-11 |
| btfnt | 2010-07-15 | |
| Wolf-fmbench | 2018-01-01 |
| QF_UFBVDT • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Jaroslav-Bendik-Certora | 2023-03-14 | 2023-07-06 |
| QF_UFBVLIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| CPAchecker_kInduction-SoSy_Lab | 2019-03-07 |
| QF_UFDT • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Bouvier | 2021-03-12 | 2021-07-18 |
| Barrett | 2017-04-28 | 2017-07-23 |
| QF_UFDTLIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Jaroslav-Bendik-Certora | 2023-03-14 | 2023-07-06 |
| QF_UFDTLIRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Kanig | 2020-03-06 | 2020-07-06 |
| QF_UFDTNIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Jaroslav-Bendik-Certora | 2023-03-14 | 2023-07-06 |
| certora | 2024-04-10 | 2024-07-22 |
| QF_UFFP • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| schanda | 2015-07-02 |
| QF_UFFPDTNIRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Kanig | 2020-03-06 | 2020-07-06 |
| QF_UFIDL • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Bouvier | 2021-03-12 | 2021-07-18 |
| mathsat | 2005-07-12 | |
| RTCL | 2005-07-12 | |
| TwoSquares | 2014-07-21 | |
| RDS | 2006-08-21 | |
| uclid2 | 2005-07-12 | |
| pete | 2005-07-12 | |
| uclid | 2005-07-12 | |
| pete2 | 2005-07-12 | |
| pete3 | 2006-08-21 | |
| UCLID-pred | 2006-08-21 |
| QF_UFLIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Jaroslav-Bendik-Certora | 2023-03-14 | 2023-07-06 |
| mathsat | 2005-07-12 | |
| TwoSquares | 2014-07-21 | |
| wisas | 2006-08-21 | |
| kind | ||
| blast |
| QF_UFLRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| FFT | 2014-07-21 | |
| mathsat | 2005-07-12 | |
| cpachecker-induction-svcomp14 | 2014-07-21 | |
| cpachecker-bmc-svcomp14 | 2014-07-21 |
| QF_UFNIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Jaroslav-Bendik-Certora | 2023-03-14 | 2023-07-06 |
| CLEARSY | 2019-09-06 | 2020-07-06 |
| CLEARSY | 2019-09-09 | 2020-07-06 |
| certora | 2024-04-10 | 2024-07-22 |
| 201903-Zohar-alive | 2019-07-07 | |
| TwoSquares | 2014-07-21 | |
| 201903-Zohar-ic | 2019-07-07 | |
| UltimateLTLAutomizer |
| QF_UFNRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| FFT | 2014-07-21 | |
| sqrtmodinv-hoenicke | 2023-03-28 | 2023-07-06 |
| CLEARSY | 2019-09-06 | 2020-07-06 |
| cas | 2009-08-02 |
| ABV • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| ABVFP • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| Heizmann-UltimateAutomizer | 2017-05-01 | 2017-07-23 |
| ABVFPLRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| Heizmann-UltimateAutomizer | 2017-05-01 | 2017-07-23 |
| ALIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| piVC | 2006-08-21 | |
| UltimateBuchiAutomizer |
| ANIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| AutomizerLoopAcceleration | 2024-04-13 | 2024-07-22 |
| UltimateBuchiAutomizer |
| AUFBV • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Alive2 | 2021-03-01 | 2021-07-18 |
| Alive2-partial-undef | 2021-03-01 | 2021-07-18 |
| nysm | 2023-10-02 | 2024-07-22 |
| AUFBVDTLIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| 20172804-Barrett | 2017-07-23 |
| AUFBVDTNIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| LibMLKEM | 2024-06-18 | 2025-08-11 |
| 20172804-Barrett | 2017-07-23 |
| AUFBVDTNIRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Kanig | 2020-03-06 | 2020-07-06 |
| SPARK | 2022-02-14 | 2022-08-10 |
| AUFBVFP • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Alive2 | 2021-03-01 | 2021-07-18 |
| Alive2-partial-undef | 2021-03-01 | 2021-07-18 |
| AUFDTLIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| 20172804-Barrett | 2017-07-23 | |
| uhbexamples | 2021-03-04 | 2022-08-10 |
| Y86 | 2021-03-04 | 2022-08-10 |
| AUFDTLIRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Kanig | 2020-03-06 | 2020-07-06 |
| AUFDTNIRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Kanig | 2020-03-06 | 2020-07-06 |
| AUFFPDTNIRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Kanig | 2020-03-06 | 2020-07-06 |
| AUFLIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Rodin | 2017-08-29 | 2019-07-07 |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| misc | 2006-08-21 |
| AUFLIRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| FFT | 2014-07-21 | |
| why | 2007-07-03 | |
| nasa | 2006-08-21 | |
| misc | 2006-08-21 | |
| peter | 2008-07-07 |
| AUFNIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Rodin | 2017-08-29 | 2019-07-07 |
| AUFNIRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| FFT | 2014-07-21 | |
| why | 2007-07-03 | |
| nasa | 2006-08-21 | |
| aviation | 2015-07-02 |
| BV • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| Heizmann-UltimateAutomizer | 2017-05-01 | 2017-07-23 |
| wintersteiger | 2015-07-02 | |
| Alive2 | 2021-03-01 | 2021-07-18 |
| Alive2-partial-undef | 2021-03-01 | 2021-07-18 |
| Preiner-scholl-smt08 | 2017-01-01 | 2017-07-23 |
| Preiner-cav18 | 2018-01-01 | 2018-07-14 |
| Preiner-psyco | 2017-01-01 | 2017-07-23 |
| PEak | 2021-03-30 | 2021-07-18 |
| llvm13-smtlib | 2015-07-02 | |
| Preiner-tptp | 2017-01-01 | 2017-07-23 |
| Preiner-keymaera | 2017-01-01 | 2017-07-23 |
| Preiner-UltimateAutomizer | 2017-01-01 | 2017-07-23 |
| Preiner-fmcad20 | 2020-01-01 | 2021-07-18 |
| BVFP • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| Heizmann-UltimateAutomizer | 2017-05-01 | 2017-07-23 |
| Alive2 | 2021-03-01 | 2021-07-18 |
| BVFPLRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| Heizmann-UltimateAutomizer | 2017-05-01 | 2017-07-23 |
| FP • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| Heizmann-UltimateAutomizer | 2017-05-01 | 2017-07-23 |
| Preiner | 2019-01-01 | 2019-07-07 |
| Pine | 2020-09-11 | 2021-07-18 |
| FPLRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| Heizmann-UltimateAutomizer | 2017-05-01 | 2017-07-23 |
| LIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| psyco | 2017-07-23 | |
| tptp | 2014-07-21 | |
| UltimateAutomizer | 2015-07-02 | |
| Frobenius | 2025-02-13 | 2025-08-11 |
| UltimateBuchiAutomizer |
| LRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| keymaera | 2014-07-21 | |
| tptp | 2014-07-21 | |
| scholl-smt08 | 2009-08-02 | |
| Monniaux-QE | 2010-01-01 | 2017-07-23 |
| polyv | 2023-03-31 | 2023-07-06 |
| Kopczynski-LOIS | 2016-09-30 |
| NIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| UltimateAutomizerSvcomp2019 | 2019-04-29 | 2020-07-06 |
| UltimateAutomizerSvcomp2023 | 2023-03-21 | 2023-07-06 |
| psyco | 2017-07-23 | |
| AutomizerLoopAcceleration | 2024-04-13 | 2024-07-22 |
| tptp | 2014-07-21 |
| NRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| keymaera | 2014-07-21 | |
| strassen-matrix-multiplication | 2022-02-22 | 2022-08-10 |
| cut-three-circles | 2022-02-22 | 2022-08-10 |
| UF • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| wintersteiger | 2015-07-02 | |
| CLEARSY | 2019-09-06 | 2020-07-06 |
| sledgehammer | 2014-07-21 | |
| Barrett | 2017-04-28 | 2017-07-23 |
| induction-by-reflection-schoisswohl | 2020-12-21 | 2021-07-18 |
| misc | 2006-08-21 | |
| grasshopper | 2014-07-21 |
| UFBV • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Jaroslav-Bendik-Certora | 2023-03-14 | 2023-07-06 |
| wintersteiger | 2015-07-02 | |
| Alive2 | 2021-03-01 | 2021-07-18 |
| Alive2-partial-undef | 2021-03-01 | 2021-07-18 |
| PEak | 2021-03-30 | 2021-07-18 |
| UFBVDT • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Jaroslav-Bendik-Certora | 2023-03-14 | 2023-07-06 |
| UFBVFP • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Alive2 | 2021-03-01 | 2021-07-18 |
| Alive2-partial-undef | 2021-03-01 | 2021-07-18 |
| UFBVLIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Schett | 2021-01-06 | 2021-07-18 |
| UFDT • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Barrett | 2017-04-28 | 2017-07-23 |
| induction-by-reflection-schoisswohl | 2020-12-21 | 2021-07-18 |
| UFDTLIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Jaroslav-Bendik-Certora | 2023-03-14 | 2023-07-06 |
| verus | 2024-12-11 | 2025-08-11 |
| 20172804-Barrett | 2017-07-23 | |
| Gleiss | 2019-01-01 | 2019-07-07 |
| UFDTLIRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Kanig | 2020-03-06 | 2020-07-06 |
| UFDTNIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Jaroslav-Bendik-Certora | 2023-03-14 | 2023-07-06 |
| verus | 2024-12-11 | 2025-08-11 |
| Gleiss | 2019-01-01 | 2019-07-07 |
| Barrett | 2020-12-12 |
| UFDTNIRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Kanig | 2020-03-06 | 2020-07-06 |
| UFFPDTNIRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Kanig | 2020-03-06 | 2020-07-06 |
| UFIDL • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| sledgehammer | 2014-07-21 | |
| RicartAgrawala | 2006-08-21 | |
| Burns | 2006-08-21 | |
| boogie | 2007-07-03 |
| UFLIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Jaroslav-Bendik-Certora | 2023-03-14 | 2023-07-06 |
| check | 2005-07-12 | |
| spec_sharp | 2009-08-02 | |
| psyco | 2017-07-23 | |
| sledgehammer | 2014-07-21 | |
| tptp | 2014-07-21 | |
| misc | 2006-08-21 | |
| grasshopper | 2014-07-21 | |
| RicartAgrawala | 2006-08-21 | |
| boogie | 2007-07-03 | |
| sexpr | 2011-06-30 | |
| tokeneer | 2009-08-02 | |
| simplify | 2006-08-21 | |
| simplify2 | 2007-07-03 |
| UFLRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| FFT | 2014-07-21 | |
| misc | 2006-08-21 | |
| asasp |
| UFNIA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| Jaroslav-Bendik-Certora | 2023-03-14 | 2023-07-06 |
| CLEARSY | 2019-09-06 | 2020-07-06 |
| spec_sharp | 2009-08-02 | |
| CLEARSY | 2019-09-09 | 2020-07-06 |
| vcc-havoc | 2009-08-02 | |
| psyco | 2017-07-23 | |
| Zohar-ic | 2019-01-01 | 2019-07-07 |
| Preiner | 2019-01-01 | 2019-07-07 |
| sledgehammer | 2014-07-21 | |
| lahiri-cav09-storm-queries | 2009-08-02 | |
| lemmas-zohar | 2025-04-14 | 2025-08-11 |
| Zohar-alive | 2019-01-01 | 2019-07-07 |
| UFNIRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| funcprobs | 2024-04-14 | 2024-07-22 |
| UFNRA • Charts • Solver Isomap | Generated | First Used |
|---|---|---|
| CLEARSY | 2019-09-06 | 2020-07-06 |