cvc5

Competing	yes
Single Query Track	ABV, ABVFP, ABVFPLRA, ALIA, AUFBV, AUFBVDTLIA, AUFBVDTNIA, AUFBVDTNIRA, AUFBVFP, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFFPDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, BV, BVFP, BVFPLRA, FP, FPLRA, LIA, LRA, NIA, NRA, QF_ABV, QF_ABVFP, QF_ABVFPLRA, QF_ALIA, QF_ANIA, QF_AUFBV, QF_AUFBVFP, QF_AUFLIA, QF_AUFNIA, QF_AX, QF_BV, QF_BVFP, QF_BVFPLRA, QF_DT, QF_FP, QF_FPLRA, QF_IDL, QF_LIA, QF_LIRA, QF_LRA, QF_NIA, QF_NIRA, QF_NRA, QF_RDL, QF_S, QF_SLIA, QF_SNIA, QF_UF, QF_UFBV, QF_UFDT, QF_UFDTLIRA, QF_UFFP, QF_UFFPDTNIRA, QF_UFIDL, QF_UFLIA, QF_UFLRA, QF_UFNIA, QF_UFNRA, UF, UFBV, UFBVFP, UFBVLIA, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFFPDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA
Incremental Track	ABVFPLRA, ALIA, AUFNIRA, BV, BVFP, BVFPLRA, LIA, LRA, QF_ABV, QF_ABVFP, QF_ABVFPLRA, QF_ALIA, QF_ANIA, QF_AUFBV, QF_AUFLIA, QF_BV, QF_BVFP, QF_BVFPLRA, QF_FP, QF_FPLRA, QF_LIA, QF_LRA, QF_NIA, QF_UF, QF_UFBV, QF_UFFP, QF_UFLIA, QF_UFLRA, QF_UFNIA, QF_UFNRA, UF, UFDTNIA, UFLRA, UFNIA, ANIA, QF_AUFBVLIA, QF_AUFBVNIA, QF_UFBVLIA, UFNRA
Unsat Core Track	ABV, ABVFP, ABVFPLRA, ALIA, AUFBV, AUFBVDTLIA, AUFBVDTNIA, AUFBVDTNIRA, AUFBVFP, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFFPDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, BV, BVFP, BVFPLRA, FP, FPLRA, LIA, LRA, NIA, NRA, QF_ABV, QF_ABVFP, QF_ABVFPLRA, QF_ALIA, QF_ANIA, QF_AUFBV, QF_AUFBVFP, QF_AUFLIA, QF_AUFNIA, QF_AX, QF_BV, QF_BVFP, QF_BVFPLRA, QF_DT, QF_FP, QF_FPLRA, QF_IDL, QF_LIA, QF_LIRA, QF_LRA, QF_NIA, QF_NIRA, QF_NRA, QF_RDL, QF_S, QF_SLIA, QF_SNIA, QF_UF, QF_UFBV, QF_UFDT, QF_UFDTLIRA, QF_UFFP, QF_UFFPDTNIRA, QF_UFIDL, QF_UFLIA, QF_UFLRA, QF_UFNIA, QF_UFNRA, UF, UFBV, UFBVFP, UFBVLIA, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFFPDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA
Model Validation Track	QF_BV, QF_BVFP, QF_BVFPLRA, QF_FP, QF_FPLRA, QF_IDL, QF_LIA, QF_LIRA, QF_LRA, QF_RDL, QF_UF, QF_UFBV, QF_UFFP, QF_UFIDL, QF_UFLIA, QF_UFLRA
Proof Exhibition Track	ABV, ABVFP, ABVFPLRA, ALIA, AUFBV, AUFBVDTLIA, AUFBVDTNIA, AUFBVDTNIRA, AUFBVFP, AUFDTLIA, AUFDTLIRA, AUFDTNIRA, AUFFPDTNIRA, AUFLIA, AUFLIRA, AUFNIA, AUFNIRA, BV, BVFP, BVFPLRA, FP, FPLRA, LIA, LRA, NIA, NRA, QF_ABV, QF_ABVFP, QF_ABVFPLRA, QF_ALIA, QF_ANIA, QF_AUFBV, QF_AUFBVFP, QF_AUFLIA, QF_AUFNIA, QF_AX, QF_BV, QF_BVFP, QF_BVFPLRA, QF_DT, QF_FP, QF_FPLRA, QF_IDL, QF_LIA, QF_LIRA, QF_LRA, QF_NIA, QF_NIRA, QF_NRA, QF_RDL, QF_S, QF_SLIA, QF_SNIA, QF_UF, QF_UFBV, QF_UFDT, QF_UFDTLIRA, QF_UFFP, QF_UFFPDTNIRA, QF_UFIDL, QF_UFLIA, QF_UFLRA, QF_UFNIA, QF_UFNRA, UF, UFBV, UFBVFP, UFBVLIA, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFFPDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA
Cloud Track
Parallel Track
Preliminary ID	36875(sq);36870(inc);36872(mv);39025(pe);36869(uc)
Final ID	39117;39114(inc)
Seed	5
System Description	cvc5 at the SMT Competition 2022
Variant of Submission ID
Derived from Solver
Wrapped Solvers
Website	https://cvc5.github.io
Team Members	Haniel Barbosa, Clark Barrett, Martin Brain, Gereon Kremer, Hanna Lachnitt, Makai Mann, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Yoni Zohar