cvc5

Competing	yes
Single Query Track	ABV, ABVFP, ABVFPLRA, ALIA, ANIA, 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_UFBVDT, QF_UFDT, QF_UFDTLIA, QF_UFDTLIRA, QF_UFDTNIA, QF_UFFP, QF_UFFPDTNIRA, QF_UFIDL, QF_UFLIA, QF_UFLRA, QF_UFNIA, QF_UFNRA, UF, UFBV, UFBVDT, UFBVFP, UFBVLIA, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFFPDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA
Incremental Track	ABVFPLRA, ALIA, ANIA, 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_LIA, QF_LRA, QF_NIA, QF_UF, QF_UFBV, QF_UFFP, QF_UFLIA, QF_UFLRA, QF_UFNIA, QF_UFNRA, UF, UFDTNIA, UFLRA, UFNIA, QF_AUFBVLIA, QF_AUFBVNIA, QF_UFBVLIA, UFNRA
Unsat Core Track	ABV, ABVFP, ABVFPLRA, ALIA, ANIA, 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_UFBVDT, QF_UFDT, QF_UFDTLIA, QF_UFDTLIRA, QF_UFDTNIA, QF_UFFP, QF_UFFPDTNIRA, QF_UFIDL, QF_UFLIA, QF_UFLRA, QF_UFNIA, QF_UFNRA, UF, UFBV, UFBVDT, UFBVFP, UFBVLIA, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFFPDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA
Model Validation Track	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_UF, QF_UFBV, QF_UFFP, QF_UFIDL, QF_UFLIA, QF_UFLRA, QF_UFNIA, QF_UFNRA
Proof Exhibition Track	ABV, ABVFP, ABVFPLRA, ALIA, ANIA, 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_UFBVDT, QF_UFDT, QF_UFDTLIA, QF_UFDTLIRA, QF_UFDTNIA, QF_UFFP, QF_UFFPDTNIRA, QF_UFIDL, QF_UFLIA, QF_UFLRA, QF_UFNIA, QF_UFNRA, UF, UFBV, UFBVDT, UFBVFP, UFBVLIA, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFFPDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA
Cloud Track	ABV, ABVFP, ABVFPLRA, ALIA, ANIA, 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_UFBVDT, QF_UFDT, QF_UFDTLIA, QF_UFDTLIRA, QF_UFDTNIA, QF_UFFP, QF_UFFPDTNIRA, QF_UFIDL, QF_UFLIA, QF_UFLRA, QF_UFNIA, QF_UFNRA, UF, UFBV, UFBVDT, UFBVFP, UFBVLIA, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFFPDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA
Parallel Track	ABV, ABVFP, ABVFPLRA, ALIA, ANIA, 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_UFBVDT, QF_UFDT, QF_UFDTLIA, QF_UFDTLIRA, QF_UFDTNIA, QF_UFFP, QF_UFFPDTNIRA, QF_UFIDL, QF_UFLIA, QF_UFLRA, QF_UFNIA, QF_UFNRA, UF, UFBV, UFBVDT, UFBVFP, UFBVLIA, UFDT, UFDTLIA, UFDTLIRA, UFDTNIA, UFDTNIRA, UFFPDTNIRA, UFIDL, UFLIA, UFLRA, UFNIA
Preliminary ID	44516;44517(inc)
Final ID	44737;44738(inc)
Seed	1965
System Description	cvc5 at the SMT Competition 2023
Variant of Submission ID
Derived from Solver
Wrapped Solvers
Website	https://cvc5.github.io
Team Members	Leni Aniva, Haniel Barbosa, Clark Barrett, Martin Brain, Vinícius Camillo, Gereon Kremer, Hanna Lachnitt, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Andres Nötzli, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Ying Sheng, Cesare Tinelli, Amalee Wilson, Yoni Zohar