Tobias Welp, Andreas Kuehlmann. Property Directed Reachability for QF_BV with mixed type atomic reasoning units. In 19th Asia and South Pacific Design Automation Conference, ASP-DAC 2014, Singapore, January 20-23, 2014. pages 738-743, IEEE, 2014. [doi]
Abstract is missing.