ABSTRACT. In our recent work we introduced an extension for the IPASIR interface of incremental SAT solvers. This extension, named IPASIR-UP, supports continuous interactions with the solver during SAT reasoning, allowing SMT solvers to seamlessly integrate any IPASIR-UP-compatible SAT solver as their core engine. While IPASIR-UP enables crucial interactions between SAT and theory solvers, the full potential of modern incremental SAT features, such as advanced inprocessing techniques, comprehensive proof production, and diverse search heuristics, remains largely untapped within this framework. In this talk, I will present the current landscape of embedding SAT solvers into SMT solvers via IPASIR-UP. I will highlight the currently supported features, discuss their limitations, and present some open problems and challenges that need to be addressed in the future.

This talk is based on joint work with Aina Niemetz, Mathias Preiner, Markus Kirchweger, Stefan Szeider, and Armin Biere.

ABSTRACT. Scheduling problems arise in many applications and are commonly solved with automated reasoning and constraint-based methods. We study a variant of the so-called resource-constrained cumulative scheduling problem, with a flavor of flow allocation, in which a set of workers must send workloads to a shared processing facility. The goal is to schedule the workload sent from each worker at each time step without exceeding the facility's maximum processing capacity or the storage capacities of the workers. In a central instantiation of the problem, the workers are industrial sources that produce wastewater that needs to be transferred to a treatment plant. The problem of computing a feasible schedule in a similar setting has previously been studied under the name of the wastewater treatment plant problem.

More precisely, we study the applicability of optimization modulo theories (OMT) and mixed integer programming (MIP) to solving real-world benchmarks of this scheduling problem. As our main contributions, we: i) extend a previously proposed constraint model for computing feasible schedules by e.g., allowing more flexible scheduling of the released water, ii) extend the model with several different optimization criteria, including optimizing for evenness of the workload arriving at the facility, and minimizing the makespan of the schedule, and iii) collect a new open-source dataset based on real-world wastewater flow quantities. We evaluate our model on two differently-sized time spans of the new dataset as well as on previously used benchmarks using state-of-the-art solvers in both paradigms. Our evaluation demonstrates that optimization criteria related to makespan minimization do not need to slow down the run time of the solvers. In contrast, the criteria on workload evenness are, in general, more difficult to handle.

ABSTRACT. SMT solvers are complex tools that can be hard to debug. We think that there is a need to add a layer of observability to gain a better understanding of how they work. We present our recent addition to Colibri2 to add structured traces in the TEF format, and its associated Vite/ReactJS vizualization front-end. We present the motivation behind this, the current design and some preliminary results.

ABSTRACT. Automated verifiers rely on SMT solvers as a backend for proof automation. This simplifies verification in the common case, but also creates usability challenges due to instability. Previous work proposes mitigation strategies motivated by the assumption that instability is a fundamental theoretical limitation. We conjecture that the instability experienced by verifiers today is often caused by fixable engineering problems, and is thus not fundamental. Should this be true, the more consequential approach to instability would be to identify root causes and connect them with solver improvements.

We conducted case studies on 11 deemed-unstable queries from existing verification projects and from Z3 issues, with the goal of diagnosing the root causes of instability. For all of them, instability is attributable to solver bugs, misconfigurations, or wrong expectations. We present our analysis and draw conclusions regarding better instability metrics, systematic debugging methods, interfaces that make instability explicit, and easier-to-debug SMT solvers.

ABSTRACT. The SMT-LIB benchmark library is a large set of benchmarks for SMT solvers. It is used by the annual SMT competition to evaluate SMT solvers, and by researchers to study novel solving techniques. Effective use of the benchmark library often requires access to benchmark metadata, such as as the number of user defined symbols. We present a comprehensive metadata catalog for the SMT-LIB benchmark library. It combines benchmark features with the results of all past SMT competition. Concretely, the catalog is implemented as a SQLite database. This allows users to use standard industry tools to perform queries, and the database to be distributed as a single file. In the future, the catalog will be distributed with the annual benchmark library release.

ABSTRACT. Optimization Modulo Theories (OMT) has evolved as a prominent extension of the Satisfiability Modulo Theories (SMT) paradigm, bringing optimization objectives into first-order logic constraint solving. Unlike SMT, which focuses solely on satisfiability with respect to a given theory, OMT additionally seeks to optimize a specified objective function. Several state-of-the-art SMT solvers have integrated OMT capabilities. However, no official SMT-LIB extension standard has yet been adopted for OMT. As a result, OMT benchmarks lack standardization, which hinders broader adoption and progress in the field. In this paper, we propose an extension to SMT-LIB that supports all of the different flavors of OMT found in the literature. Our goal is to foster the development of OMT solvers and applications, enable more robust, reusable, and comparable OMT solutions, and to promote the creation of standardized OMT benchmarks in SMT-LIB format for systematic and meaningful evaluation.

ABSTRACT. We propose an Instability Track for SMT-COMP to address the critical issue of solver instability in program verification. SMT solvers often exhibit significant performance variations when solving semantically equivalent queries, creating challenges for industrial adoption of SMT-based verification. We describe Mariposa, our tool that measures solver instability by creating semantics-preserving mutants of SMT queries and performing statistical analysis. The proposed track would evaluate solvers both on their ability to solve verification queries quickly and their stability across query variations. We discuss benchmark sources from Dafny, F*, and Verus verification projects, and propose concrete scoring rubrics for evaluating solver stability.