Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic

Peter Backeman, Philipp Rümmer, Aleksandar Zeljic. Interpolating bit-vector formulas using uninterpreted predicates and Presburger arithmetic. Formal Methods in System Design, 57(2):121-156, 2021. [doi]

Abstract

Abstract is missing.