"CVC5" (Cooperating Validity Checker 5), based on #Minisat, written in C++, and licensed under a 3-clause BSD license, is kind of the top #SMT solver according to the #SMT-COMP results. You can hook it up to #ABC, #CryptoMiniSat, #libpoly, #GMP, #CaDiCal, #symfpu, #CLN (the Class Library for Numbers), and #GLPK. #toread #formal-methods #SAT
on 02024-06-16#SMT-COMP winner "iProver" is a first-order theorem prover written in OCaml licensed under GPL2+. It wraps #Z3 and #Minisat #SAT solvers. #formal-methods #SMT
on 02024-06-16