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. We study the links between symbol elimination in local theory extensions and possibilities of computing uniform interpolants for ground formulae w.r.t. such theories. In contrast to approaches which only consider the problem of eliminating existentially quantified variables, we distinguish between interpreted and uninterpreted function symbols and analyze possibilities of obtaining uniform interpolants which can contain arbitrary interpreted function symbols, and uninterpreted function symbols in a given, specified set. We identify situations in which a hierarchical form of symbol elimination can be successfully used for this, and also investigate the limitations of the method we propose.

ABSTRACT. The theory of arrays, supported by virtually all SMT solvers, is one of the most important theories in program verification. The standard theory of arrays, which provides \emph{read} and \emph{write} operations, has been extended in various different ways in past research, among others by adding extensionality, constant arrays, function mapping (resulting in combinatorial array logic), counting, and projections. This paper studies array theories extended with \emph{sum constraints,} which capture properties of the sum of all elements of an integer array. The paper shows that the theory of extensional arrays extended with constant arrays and sum constraints can be decided in non-deterministic polynomial time. The decision procedure works both for finite and infinite index sorts, as long as the cardinality is fixed a priori. In contrast, adding sum constraints to combinatorial array logic gives rise to an undecidable theory. The paper concludes by studying several fragments in between standard arrays with sums and combinatorial arrays with sums, aiming at providing a complete characterization of decidable and undecidable fragments.

ABSTRACT. Program verification languages such as Dafny and F⋆ often rely heavily on Satisfiability Modulo Theories (SMT) solvers for proof automation. However, SMT-based verification suffers from instability, where semantically irrelevant changes in the source program can cause spurious proof failures. While existing mitigation techniques emphasize preemptive measures, we propose a complementary approach that focuses on diagnosing and repairing specific instances of instability-induced failures. Our key technique is a novel differential analysis to pinpoint problematic quantifiers in an unstable query. We instantiate this technique in Cazamariposas, a tool that automatically identifies such quantifiers and suggests fixes. We evaluate Cazamariposas on multiple large-scale systems verification projects written in three different program verification languages. Our results demonstrate Cazamariposas' effectiveness as an instability debugger. In the majority of cases, Cazamariposas successfully isolates the issue to a single problematic quantifier and provides a stabilizing fix.

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 Nonlinear Integer Arith- metic (NIA), utilizing accelerated hill-climbing and a new operation called feasible-sets jumping. We implement the proposed approach in the Model Constructing Satisfiability (MCSat) engine of the Yices2 solver, and empirically show its performance using the NIA benchmarks of SMT-LIB.

ABSTRACT. To check the satisfiability of (non-linear) real arithmetic formulas, modern satisfiability modulo theories (SMT) solving algorithms like NLSAT depend heavily on single cell construction, the task of generalizing a sample point to a connected subset (cell) of $\RR^n$ that contains the sample and over which a given set of polynomials is sign-invariant.

In this paper, we propose to speed up the computation and simplify the representation of the resulting cell by extending the considered set of polynomials with further linear polynomials. While this increases the total number of (smaller) cells generated throughout the algorithm, our experiments show that it can pay off when using suitable heuristics due to the interaction with Boolean reasoning.

ABSTRACT. The Vampire automated theorem prover is extended to output proofs in such a way that each inference is represented by a quantifier-free SMT instance. If every instance is unsatisfiable, the proof can be considered verified by an external SMT solver. This pragmatic form of proof checking places only a very light burden on the SMT solver, and can easily handle inferences that other systems may find difficult, such as theory inferences or extensive ground reasoning. The method is considerably easier to implement than proof formats based on small kernels and covers a greater variety of modern-day inferences.

ABSTRACT. We use SMT technology to address a class of problems involving uninterpreted functions and nonlinear real arithmetic. In particular, we focus on problems commonly found in mathematical competitions, such as the International Mathematical Olympiad (IMO), where the task is to determine all solutions to constraints on an uninterpreted function. Although these problems require only high-school-level mathematics, state-of-the-art SMT solvers often struggle with them. We propose several techniques to improve SMT performance in this setting.

ABSTRACT. We present a simple criterion for combining reduction pairs lexicographically. The criterion is applicable to arbitrary classes of reduction pairs, such as the polynomial interpretation, the matrix interpretation, and the Knuth--Bendix order. In addition, we investigate a variant of the matrix interpretation where the lexicographic order is employed instead of the usual component-wise order. Effectiveness is demonstrated by experiments and examples, including Touzet's Hydra Battle.

ABSTRACT. *Generalized Term Rewriting Systems* (GTRSs) extend Conditional Term Rewriting Systems by (i) restricting rewritings on arguments of function symbols and (ii) allowing for more general conditions in rules, namely, atoms defined by a set of Horn clauses. They are useful to model and analyze properties of computations with sophisticated languages like Maude. Huet proved that left-linear and parallel closed Term Rewriting Systems (TRSs) are confluent. In this paper, we generalize and extend Huet's results to GTRSs *without requiring left-linearity*. This improves Huet's result, as we show with some examples. Also, Huet's result entails confluence of weakly orthogonal TRSs, thus providing a syntactic criterion for proving confluence *without requiring termination*. We similarly introduce *weakly V-orthogonal* GTRSs, which are confluent. These results, implemented in the confluence tool CONFident, improve its ability to deal with context-sensitive and conditional term rewriting systems. We briefly report on this.

ABSTRACT. We lift the computability path ordering and its extensions from plain higher-order rewriting to higher-order rewriting on beta-eta-normal forms where matching modulo beta-eta is employed. The resulting order NCPO is shown to be useful on practical examples. In particular, it can handle systems where its cousin NHORPO fails even when it is used together with the powerful transformation technique of normalization. We also argue that automating NCPO efficiently is straightforward using SAT/SMT solvers whereas this cannot be said about the transformation technique of neutralization. Our prototype implementation supports automatic termination proof search for NCPO and is also the first one to automate NHORPO with neutralization.

ABSTRACT. Powerful confluence criteria for higher-order rewriting exist for left-linear systems, even in the presence of non-termination. On the other hand, confluence criteria that allow for mixing non-termination and non-left-linearity are either extremely limited or hardly usable in practice. In this paper, we study confluence criteria which explore sort information to make proving higher-order confluence possible, even in the presence of non-termination and non-left-linearity. We give many interesting examples of systems covered by our results, including a (confluent) variant of Klop's counterexample, and a calculus issuing from a dependent type theory with cumulative universes.