ddSMT 2.0: Better Delta Debugging for the SMT-LIBv2 Language and Friends
Gereon Kremer, Aina Niemetz, Mathias Preiner
Abstract
Abstract Erroneous behavior of verification back ends such as SMT solvers require effective and efficient techniques to identify, locate and fix failures of any kind. Manual analysis of large real-world inputs usually becomes infeasible due to the complex nature of these tools. Delta Debugging has emerged as a valuable technique to automatically reduce failure-inducing inputs while preserving the original erroneous behavior. We present , the successor of the delta debugger . is the current de-facto standard delta debugger for the SMT-LIBv2 language. Our tool improves and extends core concepts of and extends input language support to the entire family of SMT-LIBv2 language dialects. In addition to its ddmin -based main minimization strategy, it implements an alternative, orthogonal strategy based on hierarchical input minimization. We combine both strategies into a hybrid strategy and show that significantly improves over and other delta debugging tools for SMT-LIBv2 on real-world examples.