Theory References ¶

cvc5 supports all theories that are currently standardized in SMT-LIB. Additionally, it also implements several theories that are not (yet) standardized, or that extend beyond the respective standardized theory. Furthermore, cvc5 supports all combinations of all implemented theories as well as combinations with datatypes, quantifiers, and uninterpreted functions (as defined in the SMT-LIB standard) .