A Deeper Look at Depth: Stable Generation Accounting for Quantifier Reasoning

Can Cebeci, Nikolaj Bjørner, George Candea +1

SMT solvers make automated verification convenient. At the same time, solvers suffer from instability, whereby seemingly inconsequential changes to the input may cause a previously…