PV4 ⊧ Q3Bproduces a satisfiability result for a formulaSMT solver, decides satisfiability of quantified bit-vector formulas.
- SMT solving
- Quantified bit-vector formulas
- Binary Decision Diagrams (BDDs)
Type of toolSMT solver
Expected inputQuantified bit-vector formula
unsat indicating whether the quantified bit-vector formula was satisfiable or not.