Truncating abstraction of bit-vector operations for BDD-based SMT solvers

During the last few years, BDD -based SMT solvers proved to be competitive in deciding satisfiability of quantified bit-vector formulas. However, these solvers usually do not perform well on input formulas with complicated arithmetic. Hitherto, this problem has been alleviated by approximations reducing effective bit-widths of bit-vector variables. In this paper, we propose an orthogonal abstraction technique that works on the level of the individual instances of bitvector operations. In particular, we compute only several bits of the operation result, which may be sufficient to decide the satisfiability of the formula. Experimental results show that our BDD -based SMT solver Q3B extended with these abstractions can solve more quantified bit-vector formulas from the SMT - LIB repository than SMT solvers Boolector, CVC4, and Z3.