SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2021

Rules
Benchmarks
Tools
Specs
Parallel & Cloud Tracks
Participants
Results
Slides

cvc5 - fixed

Competing no
Single Query Track ABV, ABVFP, ABVFPLRA, ALIA, AUFBV, AUFBVDTLIA, AUFBVDTNIA, AUFBVFP, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFFPDTLIRA, AUFFPDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, LIA, LRA, NIA, NRA, QF_ALIA, QF_ANIA, QF_AUFLIA, QF_AUFNIA, QF_IDL, QF_LIA, QF_LIRA, QF_NIA, QF_NIRA, QF_S, QF_SLIA, QF_SNIA, QF_UFDTLIRA, QF_UFFPDTLIRA, QF_UFIDL, QF_UFLIA, QF_UFLRA, QF_UFNIA, QF_UFNRA, UFBV, UFBVFP, UFBVLIA, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFFPDTLIRA, UFFPDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA
Incremental Track
Unsat Core Track
Model Validation Track
Cloud Track
Parallel Track
Preliminary ID
Final ID 33963
Seed 0
System Description
Variant of Submission ID
Derived from Solver
Wrapped Solvers
Website https://cvc5.github.io/
Team Members Clark Barrett, Haniel Barbosa, Gereon Kremer, Abdal Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Noetzli, Mathias Preiner, Andrew Reynolds, Cesare Tinelli, Yoni Zohar
Contact noetzli@cs.stanford.edu