A Real-Blasting Extension of Cvc5 for Reasoning about Floating-Point Arithmetic

Explore a presentation from the VMCAI 2025 conference where Daisuke Ishii from JAIST introduces a novel floating-point arithmetic (FPA) theory solver implemented in the Cvc5 SMT solver. Learn about this alternative to the traditional bit-blasting method, which instead uses a real-blasting approach to reason about FPA formulas within a theory of real-integer arithmetic (RIA). Understand how this solver employs an axiomatization of FPA operations using conditional RIA formulas and features lazy instantiation of axiom fragments based on the solving context. The 29-minute video demonstrates how this tightly-coupled extended theory solver outperforms existing solutions for several problem types, as shown through experimental results. This talk was presented at the VMCAI conference (January 20-21, 2025) and sponsored by ACM SIGPLAN.