A Formal Model to Prove Instantiation Termination for E-matching-Based Axiomatisations (Extended Version)

Rui Ge, Ronald Garcia, Alexander J. Summers

SMT-based program analysis and verification often involve reasoning about program features that have been specified using quantifiers; incorporating quantifiers into SMT-based reas…