Beaver bit-vector decision procedure is a new SMT solver (decision procedure) for the theory of quantifier-free finite-precision bit-vector arithmetic developed by the UCLID group at UC Berkeley as the next generation of UCLID's bit-vector decision procedure.
Constant propagation and constraint propagation using an event-driven approach.