ABSTRACT. The talk will explain a naive approach to deciding the satisfiability of quantified bitvector formulae based on binary decision diagrams. We then describe techniques and improvements that make this approach competitive, namely simplifications of formulas with unconstrained variables, approximations based on effective bit-width reduction, and operation abstraction. Finally, we present some future research directions.

ABSTRACT. Quantified formulas pose a significant challenge for Satisfiability Modulo Theories (SMT) solvers due to their inherent undecidability. Existing instantiation techniques, such as e-matching, syntax-guided, model-based, conflict-based, and enumerative methods, often complement each other. This paper introduces a novel instantiation approach that dynamically learns from these techniques during solving. By treating observed instantiations as samples from a latent language, we use probabilistic context-free grammars to generate new, similar terms. Our method not only mimics successful past instantiations but also explores diversity by optionally inverting learned term probabilities, aiming to balance exploitation and exploration in quantifier reasoning.

ABSTRACT. This work investigates the relation between model-based quantifier instantiation (MBQI) and enumerative instantiation (EI) in Satisfiability Modulo Theories (SMT). MBQI operates at the semantic level and guarantees to find an counter-example to a given a non-model. However, it may lead to weak instantiations. In contrast, EI strives for completeness by systematically enumerating terms at the syntactic level. However, such terms may not be counter-examples. Here we investigate the relation between the two techniques and report on our initial experiments of the proposed algorithm that combines the two.

ABSTRACT. In the Nelson–Oppen combination method for satisfiability modulo theories, the combined theories must be stably infinite; in gentle combination, one theory has to be gentle, and the other has to satisfy a similar yet weaker property; in shiny combination, only one has to be shiny (smooth, with a computable minimal model function and the finite model property); and for polite combination, only one has to be strongly polite (smooth and strongly finitely witnessable). For each combination method, we prove that if any of its assumptions are removed, then there is no general method to combine an arbitrary pair of theories satisfying the remaining assumptions. We also prove new theory combination results that weaken the assumptions of gentle and shiny combination.

ABSTRACT. In this paper, we show various hardness results for the satisfiability of ground sets of literals in the theory of equality and uninterpreted functions (EUF) with finite cardinality constraints. It is known that this problem is NP-complete in the general case, when a domain D has a finite cardinality constraint |D| ≤ n, for any n ≥ 3. We notice that this problem stays NP-complete in the case of a single domain of cardinality 2, indicating that even the Boolean sort can be hard to handle when functions are present. It is trivial that the function-free case with Boolean sorts has good complexity, but allowing a single binary function, or (an arbitrary number of) unary functions only, makes the problem NP-complete.

ABSTRACT. Polynomials over bit-vectors, binary polynomials, are considered algebraically and it is observed that binary polynomials can be considered as a tree of subpolynomials. A construction of such subpolynomials is given. The application of these subpolynomials, along with other recent results on binary polynomials, in evaluating polynomials over bit-vectors as part of solving SMT problems is investigated. Preliminary results are given.

ABSTRACT. SMT solvers use sophisticated techniques for polynomial (linear or non-linear) integer arithmetic. In contrast, non-polynomial integer arithmetic has mostly been neglected so far. However, in the context of program verification, polynomials are often insufficient to capture the behavior of the analyzed system without resorting to approximations. In the last years, incremental linearization has been applied successfully to satisfiability modulo real arithmetic with transcendental functions. We adapt this approach to an extension of polynomial integer arithmetic with exponential functions. Here, the key challenge is to compute suitable lemmas that eliminate the current model from the search space if it violates the semantics of exponentiation. An empirical evaluation of our implementation shows that our approach is highly effective in practice.

ABSTRACT. Alt-Ergo is an SMT solver with strong ties to the deductive program verification framework Why3. It is used by industrial program verification tools such as Frama-C, TIS-Analyzer and SPARK. In this paper, we present recent developments to Alt-Ergo and its frontend, Dolmen. We describe a new bit-vector solver currently under development in Alt-Ergo that supports the arithmetic and logic operators from the SMT-LIB ``BV'' logic. We also describe the changes made to Dolmen to support version 2.7 of the SMT-LIB standard. Alt-Ergo's new bit-vector solver leverages a new constraint propagation architecture, a rewritten interval module, and standard propagators adapted to Alt-Ergo's Shostak-like combination procedure. We provide some preliminary benchmark results, and report on our experience and ongoing challenges.

ABSTRACT. The Model Constructing Satisfiability (MCSat) approach to the SMT problem extends the ideas of CDCL from the SAT level to the theory level. Like SAT, its search is driven by incrementally constructing a model by assigning concrete values to theory variables and performing theory-level reasoning to learn lemmas when conflicts arise. Therefore, the selection of values can significantly impact the search process and the solver’s performance. In this work, we propose guiding the MCSat search by utilizing assignment values discovered through local search. First, we present a theory-agnostic framework to seamlessly integrate local search techniques within the MCSat framework. Then, we highlight how to use the framework to design a search procedure for (quantifier-free) Nonlinear Integer Arithmetic (NIA), utilizing accelerated hill-climbing and a new operation called feasible-sets jumping. We implement the proposed approach in the MCSat engine of the Yices2 solver, and empirically evaluate its performance over the NIAbenchmarks of SMT-LIB.

ABSTRACT. This work presents an experimental investigation on the performance differences among various SMT solvers in generating differential cryptanalysis collisions for the SHA-2 family of cryptographic hash functions, a widely adopted hash function, critical for maintaining data integrity and security of protocols like TLS. The research involved examining different arguments with these solvers, and their effects on the overall solving performance. These findings provide both a methodological baseline and actionable insights regarding solver effectiveness tailored towards helping shape future research in automated cryptanalysis.

ABSTRACT. We present a novel logic-based concept called Space Explanations for classifying neural networks that gives provable guarantees of the behavior of the network in continuous areas of the input feature space. To automatically generate space explanations, we leverage a range of flexible Craig interpolation algorithms and unsatisfiable core generation. Based on real-life case studies, ranging from small to medium to large size, we demonstrate that the generated explanations are more meaningful than those computed by state-of-the-art.

ABSTRACT. Satisfiability Modulo Theory (SMT) solvers have advanced automated reasoning, solving complex formulas across discrete and continuous domains. Recent progress in propositional model counting motivates extending SMT capabilities toward model counting, especially for hybrid SMT formulas. Existing approaches, like bit-blasting, are limited to discrete variables, highlighting the challenge of counting solutions projected onto the discrete domain in hybrid formulas.

We introduce pact, an SMT model counter for hybrid formulas that uses hashing-based approximate model counting to estimate solutions with theoretical guarantees. pact makes a logarithmic number of SMT solver calls relative to the projection variables, leveraging optimized hash functions. pact achieves significant performance improvements over baselines on a large suite of benchmarks. In particular, out of 14,202 instances, pact successfully finished on 603 instances, while Baseline could only finish on 13 instances.

[Paper accepted to Design Automation Conference (DAC) 2025]

ABSTRACT. Program synthesis algorithms suffer serious scalability issues due to the exponential growth of the space of solutions as programs grow longer. A common way to tame this search space in programming by example is to use observational equivalence. In this work-in-progress report we discuss a method for using equivalence graphs (e-graphs) to lift observational equivalence to more general program synthesis problems. We first present a naive synthesis algorithm using an e-graph to perform bottom-up enumeration. We also propose an extension of e-graphs, using approximate equivalence guided by counterexamples. When evaluated against the state-of-the-art solver these approaches perform comparably, despite preliminary implementations. We further outline scope for improvements and further research.

ABSTRACT. Satisfiability Modulo Theory (SMT) checking is concerned with checking the satisfiability of first-order formulas with respect to some background theories. The SMT-LIB format is a standardized language for scripts expressing SMT problems.

Popular datasets of SMT-LIB scripts have been collected for benchmarking SMT solvers. Rather than focusing on evaluating SMT solvers, our work focuses on exploring how novice users write SMT-LIB scripts. We present a dataset of SMT-LIB scripts with fine-grained editing paths. The dataset consists of 2,415 editing paths with a total of 18,133 SMT-LIB scripts. All scripts were collected from a web-based interface for the Z3 SMT solver in educational settings.

We analyze the dataset in terms of sizes of scripts, errors users make, similarities of consecutive scripts, editing distances, and edit steps required to fix errors. We make the dataset and the code for computing our metrics available for future research on language design, tool support, and teaching materials.