From MBQI to Enumerative Instantiation and Back

Marek Dančo, Petra Hozzová, Mikoláš Janota

This work investigates the relation between model-based quantifier instantiation (MBQI) and enumerative instantiation (EI) in Satisfiability Modulo Theories (SMT). MBQI operates at…