Reasoning About Vectors using an SMT Theory of Sequences

Dynamic arrays, also referred to as vectors, are fundamental data structures used in many programs. Modeling their semantics efficiently is crucial when reasoning about such programs. The theory of arrays is widely supported but is not ideal, because the number of elements is fixed (determined by its index sort) and cannot be adjusted, which is a problem, given that the length of vectors often plays an important role when reasoning about vector programs. In this paper, we propose reasoning about vectors using a theory of sequences. We introduce the theory, propose a basic calculus adapted from one for the theory of strings, and extend it to efficiently handle common vector operations. We prove that our calculus is sound and show how to construct a model when it terminates with a saturated configuration. Finally, we describe an implementation of the calculus in cvc5 and demonstrate its efficacy by evaluating it on verification conditions for smart contracts and benchmarks derived from existing array benchmarks.


Introduction
Generic vectors are used in many programming languages. For example, in C++'s standard library, they are provided by std::vector. Automated verification of software systems that manipulate vectors requires an efficient and automated way of reasoning about them. Desirable characteristics of any approach for reasoning about vectors include: piq expressiveness-operations that are commonly performed on vectors should be supported; piiq generality-vectors are always "vectors of" some type (e.g., vectors of integers), and so it is desirable that vector reasoning be integrated within a more general framework; solvers for satisfiability modulo theories (SMT) provide such a framework and are widely used in verification tools (see [5] for a recent survey); piiiq efficiencyfast and efficient reasoning is essential for usability, especially as verification tools are increasingly used by non-experts and in continuous integration.
Despite the ubiquity of vectors in software on the one hand and the effectiveness of SMT solvers for software verification on the other hand, there is not currently a clean way to represent vectors using operators from the SMT-LIB standard [3]. While the theory of arrays can be used, it is not a great fit because arrays have a fixed size determined by their index type. Representing a dynamic array thus requires additional modeling work. Moreover, to reach an acceptable level of expressivity, quantifiers are needed, which often makes the reasoning engine less efficient and robust. Indeed, part of the motivation for this work was frustration with array-based modeling in the Move Prover, a verification framework for smart contracts [24] (see Section 6 for more information about the Move Prover and its use of vectors). The current paper bridges this gap by studying and implementing a native theory of sequences in the SMT framework, which satisfies the desirable properties for vector reasoning listed above . We present two SMT-based calculi for determining satisfiability in the theory of sequences. Since the decidability of even weaker theories is unknown (see, e.g., [9,16]), we do not aim for a decision procedure. Rather, we prove model and solution soundness (that is, when our procedure terminates, the answer is correct). Our first calculus leverages techniques for the theory of strings. We generalize these techniques, lifting rules specific to string characters to more general rules for arbitrary element types. By itself, this base calculus is already quite effective. However, it misses opportunities to perform high-level vector-based reasoning. For example, both reading from and updating a vector are very common operations in programming, and reasoning efficiently about the corresponding sequence operators is thus crucial. Our second calculus addresses this gap by integrating reasoning methods from array solvers (which handle reads and updates efficiently) into the first procedure. Notice, however, that this integration is not trivial, as it must handle novel combinations of operators (such as the combination of update and read operators with concatenation) as well as out-of-bounds cases that do not occur with ordinary arrays. We have implemented both variants of our calculus in the cvc5 SMT solver [2] and evaluated them on benchmarks originating from the Move prover, as well as benchmarks that were translated from SMT-LIB array benchmarks.
As is typical, both of our calculi are agnostic to the sort of the elements in the sequence. Reasoning about sequences of elements from a particular theory can then be done via theory combination methods such as Nelson-Oppen [19] or polite combination [17,21]. The former can be done for stably infinite theories (and the theory of sequences that we present here is stably infinite), while the latter requires investigating the politeness of the theory, which we expect to do in future work.
The rest of the paper is organized as follows. Section 2 includes basic notions from first-order logic. Section 3 introduces the theory of sequences and shows how it can be used to model vectors. Section 4 presents calculi for this theory and discusses their correctness. Section 5 describes the implementation of these calculi in cvc5. Section 6 presents an evaluation comparing several variations of the sequence solver in cvc5 and Z3. We conclude in Section 7 with directions for further research.
Related work: Our work crucially builds on a proposal by Bjørner et al. [8], but extends it in several key ways. First, their implementation (for a logic they call QF_BVRE) restricts the generality of the theory by allowing only bit-vector elements (representing characters) and assuming that sequences are bounded. In contrast, our calculus maintains full generality, allowing unbounded sequences and elements of arbitrary types. Second, while our core calculus focuses only on a subset of the operators in [8], our implementation supports the remaining operators by reducing them to the core operators, and also adds native support for the update operator, which is not included in [8].
The base calculus that we present for sequences builds on similar work for the theory of strings [6,18]. We extend our base calculus to support array-like reasoning based on the weak-equivalence approach [10]. Though there exists some prior work on extending the theory of arrays with more operators and reasoning about length [1,13,15], this work does not include support for most of the of the sequence operators we consider here.
The SMT-solver Z3 [11] also provides a solver for sequences. However, its documentation is limited [7], it does not support update directly, and its internal algorithms are not described in the literature. Furthermore, as we show in Section 6, the performance of the Z3 implementation is generally inferior to our implementation in cvc5.  with ' P tą, ă, ďu, as syntactic sugar for the equivalent literal expressed using ď (and possibly ). The sequence symbols are given on the remaining lines. Their arities are also given in Figure 1. Notice that``¨¨¨``is a variadic function symbol.

Symbol
Interpretations M of T Seq interpret: Int as the set of integers; Elem as some set; Seq as the set of finite sequences whose elements are from Elem; as the empty sequence; unit as a function that takes an element from MpElemq and returns the sequence that contains only that element; nth as a function that takes an element s from MpSeqq and an integer i and returns the ith element of s, in case i is non-negative and is smaller than the length of s (we take the first element of a sequence to have index 0). Otherwise, the function has no restrictions; update as a function that takes an element s from MpSeqq, an integer i, and an element a from MpElemq and returns the sequence obtained from s by replacing its ith element by a, in case i is non-negative and smaller than the length of s. Otherwise, the returned value is s itself; extract as a function that takes a sequence s and integers i and j, and returns the maximal sub-sequence of s that starts at index i and has length at most j, in case both i and j are non-negative and i is smaller than the length of s. Otherwise, the returned value is the empty sequence; 1 | | as a function that takes a sequence and returns its length; and``¨¨¨``as a function that takes some number of sequences (at least 2) and returns their concatenation.
Notice that the interpretations of Elem and nth are not completely fixed by the theory: Elem can be set arbitrarily, and nth is only defined by the theory for some values of its second argument. For the rest, it can be set arbitrarily.

Vectors as Sequences
We show the applicability of T Seq by using it for a simple verification task. Consider the C++ function swap at the top of Figure 2. This function swaps two elements in a vector. The comments above the function include a partial specification for it: if both indexes are in-bounds and the indexed elements are equal, then the function should not change the vector (this is expressed by s_out==s). We now consider how to encode the verification condition induced by the code and the specification. The function variables a, b, i, and j can be encoded as variables of sort Int with the same names. We include two copies of s: s for its value at the beginning, and s out for its value at the end. But what should be the sorts of s and s out ? In Figure 2 we consider two options: one is based on arrays and the other on sequences.
Example 1 (Arrays). The theory of arrays includes three sorts: index, element (in this case, both are Int), and an array sort Arr, as well as two operators: xris, interpreted as the ith element of x; and xri Ð as, interpreted as the array obtained from x by setting the element at index i to a. We declare s and s out as variables of an uninterpreted sort V and declare two functions and c, which, given v of sort V , return its length (of sort Int) and content (of sort Arr), respectively. 2 Next, we introduce functions to model vector operations: « A for comparing vectors, nth A for reading from them, and update A for updating them. These functions need to be axiomatized. We include two axioms (bottom of Figure 2): Ax 1 states that two vectors are equal iff they have the same length and the same contents. Ax 2 axiomatizes the update operator; the result has the same length, and if the updated index is in bounds, then the corresponding element is updated. These axioms are not meant to be complete, but are rather just strong enough for the example.
The first two lines of the swap function are encoded as equalities using nth A , and the last two lines are combined into one nested constraint that involves update A . The precondition of the specification is naturally modeled using nth A , and the postcondition is negated, so that the unsatisfiability of the formula entails the correctness of the function w.r.t. the specification. Indeed, the conjunction of all formulas in this encoding is unsatisfiable in the combined theories of arrays, integers, and uninterpreted functions.
The above encoding has two main shortcomings: It introduces auxiliary symbols, and it uses quantifiers, thus reducing clarity and efficiency. In the next example, we see how using the theory of sequences allows for a much more natural and succinct encoding.
Example 2 (Sequences). In the sequences encoding, s and s out have sort Seq. No auxiliary sorts or functions are needed, as the theory symbols can be used directly. Further, these symbols do not need to be axiomatized as their semantics is fixed by the theory. The resulting formula, much shorter than in Example 2 and with no quantifiers, is unsatisfiable in T Seq .

Calculi
After introducing some definitions and assumptions, we describe a basic calculus for the theory of sequences, which adapts techniques from previous procedures for the theory  of strings. In particular, the basic calculus reduces the operators nth and update by introducing concatenation terms. We then show how to extend the basic calculus by introducing additional rules inspired by solvers for the theory of arrays; the modified calculus can often reason about nth and update terms directly, avoiding the introduction of concatenation terms (which are typically expensive to reason about). Given a vector of sequence terms t " pt 1 , . . . , t n q, we use t to denote the term corresponding to the concatenation of t 1 , . . . , t n . If n " 0, t denotes , and if n " 1, t denotes t 1 ; otherwise (when n ą 1), t denotes a concatenation term having n children. In our calculi, we distinguish between sequence and arithmetic constraints.

Definition 1.
A Σ Seq -formula ϕ is a sequence constraint if it has the form s « t or s ff t; it is an arithmetic constraint if it has the form s « t, s ě t, s ff t, or s ă t where s, t are terms of sort Int, or if it is a disjunction c 1 _ c 2 of two arithmetic constraints.
Notice that sequence constraints do not have to contain sequence terms (e.g., x « y where x, y are Elem-variables). Also, equalities and disequalities between terms of sort Int are both sequence and arithmetic constraints. In this paper we focus on sequence constraints and arithmetic constraints. This is justified by the following lemma. (Proofs of this lemma and later results can be found in the appendix.) Lemma 1. For every quantifier-free Σ Seq -formula ϕ, there are sets S 1 , . . . , S n of sequence constraints and sets A 1 , . . . , A n of arithmetic constraints such that ϕ is T Seqsatisfiable iff S i Y A i is T Seq -satisfiable for some i P r1, ns. Throughout the presentation of the calculi, we will make a few simplifying assumptions.
Assumption 1. Whenever we refer to a set S of sequence constraints, we assume: 1. for every non-variable term t P T pSq, there exists a variable x such that x « t P S; 2. for every Seq-variable x, there exists a variable x such that x « |x| P S; 3. all literals in S are flat. Whenever we refer to a set of arithmetic constraints, we assume all its literals are flat.
These assumptions are without loss of generality as any set can easily be transformed into an equisatisfiable set satisfying the assumptions by the addition of fresh variables and equalities. Note that some rules below introduce non-flat literals. In such cases, we assume that similar transformations are done immediately after applying the rule to maintain the invariant that all literals in S Y A are flat. Rules may also introduce fresh variables k of sort Seq. We further assume that in such cases, a corresponding constraint k « |k| is added to S with a fresh variable k .

Definition 2.
Let C be a set of constraints. We write C |ù ϕ to denote that C entails formula ϕ in the empty theory, and write " C to denote the binary relation over T pCq such that s " C t iff C |ù s « t.

Lemma 2.
For all set S of sequence constraints, " S is an equivalence relation; furthermore, every equivalence class of " S contains at least one variable.
We denote the equivalence class of a term s according to " S by rss " S and drop the " S subscript when it is clear from the context.
In the presentation of the calculus, it will often be useful to normalize terms to what will be called a reduced form.
Definition 3. Let t be a Σ Seq -term. The reduced form of t, denoted by tÓ, is the term obtained by applying the rewrite rules listed in Figure 3 to completion.
Observe that tÓ is well defined because the given rewrite rules form a terminating rewrite system. This can be seen by noting that each rule reduces the number of applications of sequence operators in the left-hand side term or keeps that number the same but reduces the size of the term. It is not difficult to show that |ù T Seq t « tÓ.
We now introduce some basic definitions related to concatenation terms.

Definition 4.
A concatenation term is a term of the form s 1`¨¨¨`sn with n ě 2.
If each s i is a variable, it is a variable concatenation term. For a set S of sequence constraints, a variable concatenation term x 1`¨¨¨`xn is singular in S if S * x i « for at most one variable x i with i P r1, ns. A sequence variable x is atomic in S if S * x « and for all variable concatenation terms s P T pSq such that S |ù x « s, s is singular in S.
We lift the concept of atomic variables to atomic representatives of equivalence classes.
Definition 5. Let S be a set of sequence constraints. Assume a choice function α : T pSq{" S Ñ T pSq that chooses a variable from each equivalence class of " S . A sequence variable x is an atomic representative in S if it is atomic in S and x " αprxs " S q.
Finally, we introduce a relation that is the foundation for reasoning about concatenations.
Definition 6. Let S be a set of sequence constraints. We inductively define a relation S |ù``x « s, where x is a sequence variable in S and s is a sequence term whose variables are in T pSq, as follows: 1. S |ù``x « x for all sequence variables x P T pSq.

2.
S |ù``x « t for all sequence variables x P T pSq and variable concatenation terms t, where x « t P S. 3. If S |ù``x « pw``y``zqÓ and S |ù y « t and t is or a variable concatenation term in S that is not singular in S, then S |ù``x « pw``t``zqÓ. Let α be a choice function for S as defined in Definition 5. We additionally define the entailment relation S |ù˚`x « y, where y is of length n ě 0, to hold if each element of y is an atomic representative in S and there exists z of length n such that S |ù``x « z and S |ù y i « z i for i P r1, ns.
In other words, S |ù˚`x « t holds when t is a concatenation of atomic representatives and is entailed to be equal to x by S. In practice, t is determined by recursively expanding concatenations using equalities in S until a fixpoint is reached. Example 3. Suppose S " tx « y``z, y « w``u, u « vu (we omit the additional constraints required by Assumption 1, part 2 for brevity). It is easy to see that u, v, w, and z are atomic in S, but x and y are not. Furthermore, w and z (and one of u or v) must also be atomic representatives. Clearly, S |ù``x « x and S |ù x « y``z. Moreover, y``z is a variable concatenation term that is not singular in S. Hence, we have S |ù``x « py``zqÓ, and so S |ù``x « y``z (by using either Item 2 or Item 3 of Definition 6, as in fact x « y``z P S. ). Now, since S |ù``x « y``z, S |ù y « w``u, and w``u is a variable concatenation term not singular in S, we get that S |ù``x « ppw``uq``zqÓ, and so S |ù``x « w``u``z. Now, assume that v " αprvs " S q " αptv, uuq. Then, S |ù˚`x « w``v``z.
Our calculi can be understood as modeling abstractly a cooperation between an arithmetic subsolver and a sequence subsolver. Many of the derivation rules lift those in the string calculus of Liang et al. [18] to sequences of elements of an arbitrary type. We describe them similarly as rules that modify configurations.

Definition 7.
A configuration is either the distinguished configuration unsat or a pair pS, Aq of a set S of sequence constraints and a set A of arithmetic constraints.
The rules are given in guarded assignment form, where the rule premises describe the conditions on the current configuration under which the rule can be applied, and the conclusion is either unsat, or otherwise describes the resulting modifications to the configuration. A rule may have multiple conclusions separated by . In the rules, some of the premises have the form S |ù s « t (see Definition 2). Such entailments can be checked with standard algorithms for congruence closure. Similarly, premises of the form S |ù LIA s « t can be checked by solvers for linear integer arithmetic.
An application of a rule is redundant if it has a conclusion where each component in the derived configuration is a subset of the corresponding component in the premise configuration. We assume that for rules that introduce fresh variables, the introduced variables are identical whenever the premises triggering the rule are the same (i.e., we cannot generate an infinite sequence of rule applications by continuously using the same premises to introduce fresh variables). 3 A configuration other than unsat is saturated with respect to a set R of derivation rules if every possible application of a rule in R to it is redundant. A derivation tree is a tree where each node is a configuration whose children, if any, are obtained by a non-redundant application of a rule of the calculus. A derivation tree is closed if all of its leaves are unsat. As we show later, a closed derivation tree with root node pS, Aq is a proof that A Y S is unsatisfiable in T Seq . In contrast, a derivation tree with root node pS, Aq and a saturated leaf with respect to all the rules of the calculus is a witness that A Y S is satisfiable in T Seq .

Basic Calculus Definition 8. The calculus BASE consists of the derivation rules in Figures 4 and 5.
Some of the rules are adapted from previous work on string solvers [18,23]. Compared to that work, our presentation of the rules is noticeably simpler, due to our use of the relation |ù˚`from Definition 6. In particular, our configurations consist only of pairs of sets of formulas, without any auxiliary data-structures.
Note that judgments of the form S |ù˚`x « t are used in premises of the calculus. It is possible to compute whether such a premise holds thanks to the following lemma.
Lemma 3. Let S be a set of sequence constraints and A a set of arithmetic constraints. If pS, Aq is saturated w.r.t. S-Prop, L-Intro and L-Valid, the problem of determining whether S |ù˚`x « s for given x and s is decidable.
Lemma 3 assumes saturation with respect to certain rules. Accordingly, our proof strategy, described in Section 5, will ensure such saturation before attempting to apply rules relying on |ù˚`. The relation |ù˚`induces a normal form for each equivalence class of " S . Lemma 4. Let S be a set of sequence constraints and A a set of arithmetic constraints. Suppose pS, Aq is saturated w.r.t. A-Conf, S-Prop, L-Intro, L-Valid, and C-Split. Then, for every equivalence class e of " S whose terms are of sort Seq, there exists a unique (possibly empty) s such that whenever S |ù˚`x « s 1 for x P e, then s 1 " s. In this case, we call s the normal form of e (and of x). We now turn to the description of the rules in Figure 4, which form the core of the calculus. For greater clarity, some of the conclusions of the rules include terms before they are flattened. First, either subsolver can report that the current set of constraints is unsatisfiable by using the rules A-Conf or S-Conf. For the former, the entailment |ù LIA (which abbreviates |ù T LIA ) can be checked by a standard procedure for linear integer arithmetic, and the latter corresponds to a situation where congruence closure detects a conflict between an equality and a disequality. The rules A-Prop, S-Prop, and S-A correspond to a form of Nelson-Oppen-style theory combination between the two subsolvers. The first two communicate equalities between the sub-solvers, while the third guesses arrangements for shared variables of sort Int. L-Intro ensures that the length term |s| for each sequence term s is equal to its reduced form p|s|qÓ. L-Valid restricts sequence lengths to be non-negative, splitting on whether each sequence is empty or has a length greater than 0. The unit operator is injective, which is captured by U-Eq. C-Eq concludes that two sequence terms are equal if they have the same normal form. If two sequence variables have different normal forms, then C-Split takes the first differing components y and y 1 from the two normal forms and splits on their length relationship. Note that C-Split is the source for non-termination of the calculus (see, e.g., [18,23]). Finally, Deq-Ext handles disequalities between sequences x and y by either asserting that their lengths are different or by choosing an index i at which they differ. Figure 5 includes a set of reduction rules for handling operators that are not directly handled by the core rules. These reduction rules capture the semantics of these operators by reduction to concatenation. R-Extract splits into two cases: Either the extraction uses 5: Reduction rules for extract, nth, and update. The rules use k, k 1 , and k 2 to denote fresh sequence variables. We write s « minpt, uq as an abbreviation for s « t _ s « u, s ď t, s ď u.

A-Conf
an out-of-bounds index or a non-positive length, in which case the result is the empty sequence, or the original sequence can be described as a concatenation that includes the extracted sub-sequence. R-Nth creates an equation between y and a concatenation term with unitpxq as one of its components, as long as i is not out of bounds. R-Update considers two cases. If i is out of bounds, then the update term is equal to y. Otherwise, y is equal to a concatenation, with the middle component (k 1 ) representing the part of y that is updated. In the update term, k 1 is replaced by unitpzq.
Example 4. Consider a configuration pS, Aq, where S contains the formulas x « y``z, z « v``x``w, and v « unitpuq, and A is empty. Hence, S |ù |x| « |y``z|. By L-Intro, we have S |ù |y``z| « |y|`|z|. Together with Assumption 1, we have S |ù x « y` z , and then with S-Prop, we have x « y` z P A. Similarly, we can derive z « v` x` w , v « 1 P S, and so p˚q A |ù LIA z « 1` y` z` w . Notice that for any variable k of sort Seq, we can apply L-Valid, L-Intro, and S-Prop to add to A either k ą 0 or k " 0. Applying this to y, z, w, we have that A |ù LIA K in each branch thanks to p˚q, and so A-Conf applies and we get unsat.

Extended Calculus
Definition 9. The calculus EXT is comprised of the derivation rules in Figures 4 and 6, with the addition of rule R-Extract from Figure 5.
Our extended calculus combines array reasoning, based on [10] and expressed by the rules in Figure 6, with the core rules of Figure 4 and the R-Extract rule. Unlike in BASE, those rules do not reduce nth and update. Instead, they reason about those operators directly and handle their combination with concatenation. Nth-Concat identifies the ith element of sequence y with the corresponding element selected from its normal form (see Lemma 4). Update-Concat operates similarly, applying update to all the components.
Update-Concat-Inv operates similarly on the updated sequence rather than on the original sequence. Nth-Unit captures the semantics of nth when applied to a unit term. Update-Unit is similar and distinguishes an update on an out-of-bounds index (different from 0) from an update within the bound. Nth-Intro is meant to ensure that Nth-Update (explained below) and Nth-Unit (explained above) are applicable whenever an update term exists in the constraints. Nth-Update captures the read-over-write axioms of arrays, adapted to consider their lengths (see, e.g., [10]). It distinguishes three cases: In the first, the update index is out of bounds. In the second, it is not out of bounds, and the corresponding nth term accesses the same index that was updated. In the third case, the index used in the nth term is different from the updated index. Update-Bound considers two cases: either the update changes the sequence, or the sequence remains the same. Finally, Nth-Split introduces a case split on the equality between two sequence variables x and x 1 whenever they appear as arguments to nth with equivalent second arguments. This is needed to ensure that we detect all cases where the arguments of two nth terms must be equal.

Correctness
In this section we prove the following theorem: Theorem 1. Let X P tBASE, EXTu and pS 0 , A 0 q be a configuration, and assume without loss of generality that A 0 contains only arithmetic constraints that are not sequence constraints. Let T be a derivation tree obtained by applying the rules of X with pS 0 , A 0 q as the initial configuration. 1 If T contains a saturated configuration pS, Aq w.r.t. X, then pS, Aq is T Seq -satisfiable, and so is pS 0 , A 0 q.
The theorem states that the calculi are correct in the following sense: if a closed derivation tree is obtained for the constraints S 0 Y A 0 then those constraints are unsatisfiable in T Seq ; if a tree with a saturated leaf is obtained, then they are satisfiable. It is possible, however, that neither kind of tree can be derived by the calculi, making them neither refutation-complete nor terminating. This is not surprising since, as mentioned in the introduction, the decidability of even weaker theories is still unknown.
Proving the first claim in Theorem 1 reduces to a local soundness argument for each of the rules. For the second claim, we sketch below how to construct a satisfying model M from a saturated configuration for the case of EXT. The case for BASE is similar and simpler.
Model construction steps The full model construction and its correctness are described in the appendix together with a proof of the theorem above. Here is a summary of the steps needed for the model construction. 1. Sorts: MpElemq is interpreted as some arbitrary countably infinite set. MpSeqq and MpIntq are then determined by the theory. 2. Σ Seq -symbols: T Seq enforces the interpretation of almost all Σ Seq -symbols, except for nth when the second input is out of bounds. We cover this case below. 3. Integer variables: based on the saturation of A-Conf, we know there is some T LIAmodel satisfying A. We set M to interpret integer variables according to this model.

Nth-Concat
x « nthpy, iq P S S |ù˚`y « w1``¨¨¨``wn 6: Extended derivation rules. The rules use z 1 , . . . , z n to denote fresh sequence variables and e, e 1 to denote fresh element variables. 4. Element variables: these are partitioned into their " S equivalence classes. Each class is assigned a distinct element from MpElemq, which is possible since it is infinite. 5. Atomic sequence variables: these are assigned interpretations in several sub-steps: (a) length: we first use the assignments to variables x to set the length of Mpxq, without assigning its actual value. (b) unit variables: for variables x with x " S unitpzq, we set Mpxq to be rMpzqs. (c) non-unit variables: All other sequence variables are assigned values according to a weak equivalence graph we construct in a manner similar to [10]. This construction takes into account constraints that involve update and nth. 6. Non-atomic sequence variables: these are first transformed to their unique normal form (see Lemma 4), consisting of concatenations of atomic variables. Then, the values assigned to these variables are concatenated. 7. nth-terms: for out-of-bounds indices in nth-terms, we rely on " S to make sure that the assignment is consistent. We conclude this section with an example of the construction of M.
Example 5. Consider a signature in which Elem is Int, and a saturated configuration pS˚, A˚q w.r.t. EXT that includes the following formulas: y « y 1`y2 , x « x 1`x2 , y 2 « x 2 , y 1 « updatepx 1 , i, aq, |y 1 | " |x 1 |, |y 2 | " |x 2 |, nthpy, iq « a, nthpy 1 , iq « a. Following the above construction, a satisfying interpretation M can be built as follows: Step 1 Set both MpIntq and MpElemq to be the set of integer numbers. MpSeqq is fixed by the theory.
Step 5a Start assigning values to sequences. First, set the lengths of Mpxq and Mpyq to be 4, and the lengths of Mpx 1 q, Mpx 2 q, Mpy 1 q, Mpy 2 q to be 2.
Step 5b is skipped as there are no unit terms.
Step 7 No integer variable in the formula was assigned an out-of-bound value, and so the interpretation of nth on out-of-bounds cases is set arbitrarily.

Implementation
We implemented our procedure for sequences as an extension of a previous theory solver for strings [18,23]. This solver is integrated in cvc5, and has been generalized to reason about both strings and sequences. In this section, we describe how the rules of the calculus are implemented and the overall strategy for when they are applied. Like most SMT solvers, cvc5 is based on the CDCLpT q architecture [20] which combines several subsolvers, each specialized on a specific theory, with a solver for propositional satisfiability (SAT). Following that architecture, cvc5 maintains an evolving set of formulas F. When F starts with quantifier-free formulas over the theory T Seq , the case targeted by this work, the SAT solver searches for a satisfying assignment for F, represented as the set M of literals it satisfies. If none exists, the problem is unsatisfiable at the propositional level and hence T Seq -unsatisfiable. Otherwise, M is partitioned into the arithmetic constraints A and the sequence constraints S and checked for T Seq -satisfiability using the rules of the EXT calculus. Many of those rules, including all those with multiple conclusions, are implemented by adding new formulas to F (following the splitting-on-demand approach [4]). This causes the SAT solver to try to extend its assignment to those formulas, which results in the addition of new literals to M (and thereby also to A and S).
In this setting, the rules of the two calculi are implemented as follows. The effect of rule A-Conf is achieved by invoking cvc5's theory solver for linear integer arithmetic. Rule S-Conf is implemented by the congruence closure submodule of the theory solver for sequences. Rules A-Prop and S-Prop are implemented by the standard mechanism for theory combination. Note that each of these four rules may be applied eagerly, that is, before constructing a complete satisfying assignment M for F.
The remaining rules are implemented in the theory solver for sequences. Each time M is checked for satisfiability, cvc5 follows a strategy to determine which rule to apply next. If none of the rules apply and the configuration is different from unsat, then it is saturated, and the solver returns sat. The strategy for EXT prioritizes rules as follows.
Only the first applicable rule is applied (and then control goes back to the SAT solver). 1. (Add length constraints) For each sequence term in S, apply L-Intro or L-Valid, if not already done. We apply L-Intro for non-variables, and L-Valid for variables. 2. (Mark congruent terms) For each set of update (resp. nth) terms that are congruent to one another in the current configuration, mark all but one term and ignore the marked terms in the subsequent steps. 3. (Reduce extract) For extractpy, i, jq in S, apply R-Extract if not already done. 4. (Construct normal forms) Apply U-Eq or C-Split. We choose how to apply the latter rule based on constructing normal forms for equivalence classes in a bottomup fashion, where the equivalence classes of x and y are considered before the equivalence class of x``y. We do this until we find an equivalence class such that S |ù˚`z « u 1 and S |ù˚`z « u 2 for distinct u 1 , u 2 . 5. (Normal forms) Apply C-Eq if two equivalence classes have the same normal form. 6 Apply Nth-Split to pairs of nth terms with equivalent indices. 9. (Theory combination) Apply S-A for all arithmetic terms occurring in both S and A. Whenever a rule is applied, the strategy will restart from the beginning in the next iteration. The strategy is designed to apply with higher priority steps that are easy to compute and are likely to lead to conflicts. Some steps are ordered based on dependencies from other steps. For instance, Steps 5 and 7 use normal forms, which are computed in Step 4. The strategy for the BASE calculus is the same, except that Steps 7 and 8 are replaced by one that applies R-Update and R-Nth to all update and nth terms in S.
We point out that the C-Split rule may cause non-termination of the proof strategy described above in the presence of cyclic sequence constraints, for instance, constraints where sequence variables appear on both sides of an equality. The solver uses methods for detecting some of these cycles, to restrict when C-Split is applied. In particular, when S |ù˚`x « pu``s``wqÓ, S |ù˚`x « pu``t``vqÓ, and s occurs in v, then C-Split is not applied. Instead, other heuristics are used, and in some cases the solver terminates with a response of "unknown" (see e.g., [18] for details). In addition to the version shown here, we also use another variation of the C-Split rule where the normal forms are matched in reverse (starting from the last terms in the concatenations). The implementation also uses fast entailment tests for length inequalities. These tests may allow us to conclude which branch of C-Split, if any, is feasible, without having to branch on cases explicitly.
Although not shown here, the calculus can also accommodate certain extended sequence constraints, that is, constraints using a signature with additional functions. For example, our implementation supports sequence containment, replacement, and reverse. It also supports an extended variant of the update operator, in which the third argument is a sequence that overrides the sequence being updated starting from the index given in the second argument. Constraints involving these functions are handled by reduction rules, similar to those shown in Figure 5. The implementation is further optimized by using context-dependent simplifications, which may eagerly infer when certain sequence terms can be simplified to constants based on the current set of assertions [23].

Evaluation
We evaluate the performance of our approach, as implemented in cvc5. The evaluation investigates: (i) whether the use of sequences is a viable option for reasoning about vectors in programs, (ii) how our approach compares with other sequence solvers, and (iii) what is the performance impact of our array-style extended rules. As a baseline, we use Version 4.8.14 of the Z3 SMT solver, which supports a theory of sequences without updates. For cvc5, we evaluate implementations of both the basic calculus (denoted cvc5) and the extended array-based calculus (denoted cvc5-a). The benchmarks, solver configurations, and logs from our runs are available for download. 4 We ran all experiments on a cluster equipped with Intel Xeon E5-2620 v4 CPUs. We allocated one physical CPU core and 8GB of RAM for each solver-benchmark pair and used a time limit of 300 seconds. We use the following two sets of benchmarks: Array Benchmarks (ARRAYS) The first set of benchmarks is derived from the QF_AX benchmarks in SMT-LIB [3]. To generate these benchmarks, we (i) replace declarations of arrays with declarations of sequences of uninterpreted sorts, (ii) change the sort of index terms to integers, and (iii) replace store with update and select with nth. The resulting benchmarks are quantifier-free and do not contain concatenations. Note that the original and the derived benchmarks are not equisatisfiable, because sequences take into account out-of-bounds cases that do not occur in arrays. For the Z3 runs, we add to the benchmarks a definition of update in terms of extraction and concatenation.

Smart Contract Verification (DIEM)
The second set of benchmarks consists of verification conditions generated by running the Move Prover [24] on smart contracts written for the Diem framework. By default, the encoding does not use the sequence update operation, and so Z3 can be used directly. However, we also modified the Move Prover encoding to generate benchmarks that do use the update operator, and ran cvc5 on them. In addition to using the sequence theory, the benchmarks make heavy use of quantifiers and the SMT-LIB theory of datatypes. largest number of benchmarks is the implementation of the extended calculus (cvc5-a). This approach also successfully solves most of the DIEM benchmarks, which suggests that sequences are a promising option for encoding vectors in programs. The results further show that the sequences solver of cvc5 significantly outperforms Z3 on both the number of solved benchmarks and the solving time on commonly solved benchmarks. Figures 7b and 7c show scatter plots comparing cvc5 and cvc5-a on the two benchmark sets. We can see a clear trend towards better performance when using the extended solver. In particular, the table shows that in addition to solving the most benchmarks, cvc5-a is also fastest on the commonly solved instances from the DIEM benchmark set.
For the ARRAYS set, we can see that some benchmarks are slower with the extended solver. This is also reflected in the table, where cvc5-a is slower on the commonly solved instances. This is not too surprising, as the extra machinery of the extended solver can sometimes slow down easy problems. As problems get harder, however, the benefit of the extended solver becomes clear. For example, if we drop Z3 and consider just the commonly solved instances between cvc5 and cvc5-a (of which there are 242), cvc5-a is about 2.47ˆfaster (426 vs 1053 seconds). Of course, further improving the performance of cvc5-a is something we plan to explore in future work.

Conclusion
We introduced calculi for checking satisfiability in the theory of sequences, which can be used to model the vector data type. We described our implementation in cvc5 and provided an evaluation, showing that the proposed theory is rich enough to naturally express verification conditions without introducing quantifiers, and that our implementation is efficient. We believe that verification tools can benefit by changing their encoding of verification conditions that involve vectors to use the proposed theory and implementation.
We plan to propose the incorporation of this theory in the SMT-LIB standard and contribute our benchmarks to SMT-LIB. As future research, we plan to integrate other approaches for array solving into our basic solver. We also plan to study the politeness [17,21] and decidability of various fragments of the theory of sequences.

A Appendix
In this appendix, each section presents a proof that was omitted from the main text due to lack of space. For convenience, the lemma/theorem that is being proved is repeated at the beginning of each section.
Below, we make use of the following helper lemma.
Lemma 5. Let S be a set of sequence constraints and A a set of arithmetic constraints. Suppose pS, Aq is saturated w.r.t. S-Prop, L-Intro and L-Valid. If x 1`¨¨¨`xn P T pSq is a variable concatenation term of size n not singular in S, then 1. A |ù LIA Σ n k"1 x k ě 2; and 2. for each m P r1, ns, A |ù LIA Σ n k"1 x k ą xm .
Proof. Let i, j P r1, ns, i ‰ j, such that S * x i « and S * x j « . We know that x i , x j P T pSq, so by saturation of L-Valid, we have A |ù xi ą 0 and A |ù xj ą 0. Also, by saturation of L-Valid, L-Intro, and S-Prop, together with Assumption 1, we know that A |ù LIA x k ě 0 for k P r1, ns. It follows that A |ù LIA Σ n k"1 x k ě 2. Furthermore, for each m P r1, ns, A |ù LIA Σ n k"1 x k ą xm .

A.1 Proof of Lemma 1
Lemma 1. For every quantifier-free Σ Seq -formula ϕ, there are sets S 1 , . . . , S n of sequence constraints and sets A 1 , . . . , A n of arithmetic constraints such that ϕ is Proof. Using standard transformations, ϕ can be transformed into an equisatisfiable disjunction ϕ 1 " ϕ 1 _ . . . _ ϕ n , where for i P r1, ns, ϕ i is a conjunction ϕ 1 i , . . . , ϕ ni i of flat literals. Each flat literal in ϕ 1 is either a sequence constraint or an arithmetic constraint. For each i P r1, ns we set S i " tϕ j i | such that ϕ j i is a sequence constraint u and A i " tϕ j i | such that ϕ j i is an arithmetic constraint u. Hence, for every T Seqinterpretation M, M |ù ϕ iff M |ù S i Y A i for some i P r1, ns.

A.2 Proof of Lemma 3
Lemma 3. Let S be a set of sequence constraints and A a set of arithmetic constraints. If pS, Aq is saturated w.r.t. S-Prop, L-Intro and L-Valid, the problem of determining whether S |ù˚`x « s for given x and s is decidable. Proof. We show that the set of pairs px, sq for which S |ù``x « s is finite (it is then easy to see that the set of pairs py, tq for which S |ù˚`y « t is also finite). Consider a tree whose root is obtained by Item 1 or Item 2 of Definition 6 where the children of a node are all possible results of applying Item 3 of Definition 6. Note that each node can have only finitely many children as there are only finitely many pairs py, tq where y is a variable in S and t is or a variable concatenation term in T pSq. Below, we show that every path in the tree is finite, from which it follows that the tree is finite. Since there are only finitely many such trees, it follows that the set of px, sq for which S |ù``x « s is finite.
Define a partial order ă over terms of sort Seq in T pSq, by s ă t iff A |ù LIA xs ă xt for some variables x s and x t such that x s " S s and x t " S t. We show that ă is well defined. First, by Assumption 1, such x s and x t exist. Next, if x s " S s, x t " S t, x 1 s " S s and s and S |ù x t « x 1 t and saturation of S-Prop. Let ă˚be the (well-founded) Dershowitz-Manna multiset ordering induced by ă [12], that is, the minimal transitive relation that satisfies: A ă˚B whenever A is obtained from B by removing a single element b, and possibly adding any finite number of elements a such that a ă b for every such new element. Now, for each term t of sort Seq in T pSq, let mptq be the multiset of the terms occurring in it (the multiplicity of each element in this multiset is the number of times it occurs in t). We prove the following claim, which establishes that every path in the tree mentioned above is finite: if S |ù``x « pw``y``zqÓ, S |ù y « t and t is or a variable concatenation term in S that is not singular in S, then mppw``y``zqÓq ą˚mppw``t``zqÓq.
We consider two cases: t is or t is a variable concatenation term in T pSq not singular in S. In the first case, pw``t``zqÓ " pw``zqÓ. Note that the only role of Ó here is to flatten nested concatenations. Hence, y is removed from the multiset of sub-terms and is not replaced by anything, so mppw``y``zqÓq ą˚mppw``t``zqÓq.
In the second case, t is a variable concatenation term in S not singular in S. Let t " t 1`. . .``t n . Now, pw``pt 1`¨¨¨`tn q``zqÓ is a flat concatenation in which y was removed, and t 1 , . . . , t n were added. To prove a decrease in ă˚from mppw``y``zqÓq to mppw``t``zqÓq, we show that for every k P r1, ns, t k ă y, that is, A |ù LIA t k ă y (notice that t k and y are variables). By Lemma 5, we know that for each k P r1, ns, A |ù LIA Σ n i"1 ti ą t k . Since S |ù y « t, we have S |ù |y| " |t|. By saturation of L-Intro and S-Prop, and by Assumption 1, it follows that A |ù y " Σ n i"1 ti . Thus, A |ù LIA y ą t k .

A.3 Proof of Lemma 4
Lemma 4. Let S be a set of sequence constraints and A a set of arithmetic constraints. Suppose pS, Aq is saturated w.r.t. A-Conf, S-Prop, L-Intro, L-Valid, and C-Split. Then, for every equivalence class e of " S whose terms are of sort Seq, there exists a unique (possibly empty) s such that whenever S |ù˚`x « s 1 for x P e, then s 1 " s. In this case, we call s the normal form of e (and of x).

Proof.
Let e be an equivalence class of " S whose terms are of sort Seq, and let x P e (we know every equivalence class has at least one variable by Lemma 2). We show existence and uniqueness of a normal form for e.
Existence: We show that for some s, S |ù˚`x « s. Consider the tree construction of Lemma 3. If we follow some path in the tree, we will reach a node S |ù``x « t for which no children can be derived (i.e., Item 3 of Definition 6 doesn't apply). It is not hard to see that t " pt 1 , . . . , t n q, where n ě 0 and each t i is a variable for i P r1, ns.
Let s have the same length as t and let s i :" αpt i q for i P r1, ns. We prove that S |ù˚`x « s. We know that S |ù``x « t. If n " 0, then trivially, S |ù˚`x « s.
Otherwise, for each i P r1, ns, we further know that S |ù t i « s i and s i " αprs i sq, so it only remains to show that s i is atomic in S. Assume it is not. Then either S |ù s i « or there exists a variable concatenation term u P T pSq not singular in S such that S |ù s i « u. In either case, this would imply that Item 3 of Definition 6 is applicable to S |ù``x « t, contradicting our assumption.
Uniqueness: By the existence argument above, there exists some s such that S |ù˚x « s. Now, suppose S |ù˚`x « s 1 , and assume that s ‰ s 1 . Then there must be w, z, z 1 , y, y 1 , each containing only variables that are atomic representatives, such that s " pw``y``zqÓ and s 1 " pw``y 1`z1 qÓ, with y ‰ y 1 . By saturation w.r.t. C-Split, there are three possibilities: A |ù y ą y 1 and y « y 1`k P S for some k; A |ù y ă y 1 and y 1 « y``k P S for some k; or A |ù y " y 1 and y « y 1 P S. In the first case, notice that since S |ù y « y 1`k , it follows that S |ù |y| « |y 1`k |. Also, by saturation of L-Intro, S |ù |y 1`k | « |y 1 |`|k|. So, S |ù |y| « |y 1 |`|k|. And, by saturation of S-Prop and Assumption 1 also A |ù y « y 1` k . It follows that S * k « ; otherwise, we would have A |ù k « 0 by L-Intro and S-Prop, which together with A |ù y ą y 1 contradicts saturation of A-Conf. Also, y 1 is atomic and hence, S * y 1 « . Thus, S |ù y « y 1`k but y 1`k is not singular in S as S * k « and S * y 1 « . In particular, this means that y is not atomic, which contradicts our assumption, so the first case is impossible. The second case is analogous to the first. In the third case, we have y « y 1 P S, but we know that y and y 1 are both equivalence class representatives, so it must be that y " y 1 , which contradicts our assumption that y ‰ y 1 .
A.4 Proof of Theorem 1, Item 1 Theorem 1. Let X P tBASE, EXTu and pS 0 , A 0 q be a configuration, and assume without loss of generality that A 0 contains only arithmetic constraints that are not sequence constraints. Let T be a derivation tree obtained by applying the rules of X with pS 0 , A 0 q as the initial configuration. 1. If T is closed, then S 0 Y A 0 is T Seq -unsatisfiable. 2. If T contains a saturated configuration pS, Aq w.r.t. X, then pS, Aq is T Seq -satisfiable, and so is pS 0 , A 0 q.
The proof of Item 1 is routine, and amounts to a local soundness check of each of the derivation rules. The only non-trivial case is C-Split, which relies on the following lemma: Lemma 6. Let S be a set of sequence constraints and A a set of arithmetic constraints. Suppose pS, Aq is saturated w.r.t. S-Prop, L-Intro and L-Valid. If S |ù˚`x « s then S |ù T Seq x « s.
Proof. Suppose S |ù˚`x « s where s " ps 1 , . . . , s n q. Then, for some s 1 " ps 1 1 , . . . , s 1 n q, S |ù``x « s 1 and S |ù s i « s 1 i for i P r1, ns. To show that S |ù T Seq x « s, it thus suffices to show that S |ù T Seq x « s 1 . As shown in Lemma 3, there is a finite number k of derivation steps in |ù``that yield x « s 1 . We prove the claim by induction on k. For k " 1, we either apply Item 1 or Item 2. In the former case we get a trivial identity S |ù``x « x, and clearly S |ù T Seq x « x. In the latter case, we get an identity S |ù``x « t such that S |ù x « t, and so in particular S |ù T Seq x « t. Suppose k ą 1, and that x « s 1 was obtained using Item 3 of Definition 6. Hence, s 1 has the form pw``t``zqÓ, where S |ù``x « pw``y``zqÓ with a shorter derivation, and S |ù y « t. By the induction hypothesis, S |ù T Seq x « pw``y``zqÓ. Clearly, S |ù T Seq y « t. Hence, S |ù T Seq x « s 1 .
Using Lemma 6, since S |ù˚`x « s implies that x « s follows from S in T Seq , we have that every model of the assumptions of C-Split assigns the same values to pw``y``zqÓ and pw``y 1`z1 qÓ. Assuming that the first two branches of the conclusion do not hold in some model, we indeed get that the interpretations of y and y 1 must be identical, as they are the sub-sequence of the same sequence, that begins at the same index and whose length is the same.
A.5 Proof of Theorem 1, Item 2 Theorem 1. Let X P tBASE, EXTu and pS 0 , A 0 q be a configuration, and assume without loss of generality that A 0 contains only arithmetic constraints that are not sequence constraints. Let T be a derivation tree obtained by applying the rules of X with pS 0 , A 0 q as the initial configuration. 1. If T is closed, then S 0 Y A 0 is T Seq -unsatisfiable. 2. If T contains a saturated configuration pS, Aq w.r.t. X, then pS, Aq is T Seq -satisfiable, and so is pS 0 , A 0 q.
Consider a saturated configuration pS, Aq. We define an interpretation M. Unless stated otherwise, by equivalence class we mean an equivalence class w.r.t. " S and may drop the subscript when referring to it (e.g., writing rxs for the equivalence class of x). We also sometimes drop "in S" from "atomic in S" when S is clear from context. We say that an equivalence class e is atomic if its terms are of sort Seq and all variables in it are atomic. Note that if e contains any variable that is atomic in S, then all variables in e are atomic in S.
The following definitions completely define the model M. Concretely, Definition 10 defines the domains of M; Definition 11 defines the function symbols of Σ Seq . Definition 12 defines the interpretations of variables of sort Int and Elem; Definition 13 assigns lengths to the interpretations of variables of sort Seq that are atomic in S (it does not set their values, but only their lengths); Definition 15 defines the interpretations of variables of sort Seq that are equivalent to unit terms; Definition 18 defines the interpretations of variables of sort Seq that are atomic in S but are not equivalent to unit terms; Definition 19 defines the interpretations of variables of sort Seq that are not atomic in S; Finally, Definition 20 defines the interpretation of the nth symbol in M (note that only a part of its interpretation is fixed by the theory).
The definitions are shown to be well-defined in Lemma 10.
We start by assigning domains to the sorts of T Seq .

1.
MpIntq " Z, the set of integers. 2. MpElemq is some countably infinite set. 3. MpSeqq is the set of finite sequences whose elements are taken from MpElemq.
The domains for Int and Seq were chosen to be consistent with the requirements of T Seq . The exact identity of Elem is not important, and so we set its elements to be arbitrary. In contrast, its cardinality is important, and is set to be infinite.
Definition 11 (Model construction: function symbols). The symbols shown in Figure 1 are interpreted in such a way that M is both a T LIA -interpretation and a T Seqinterpretation, as described in Figure 1 and in Sections 2 and 3.

Now we can assign values to variables of sort Int and Elem.
Definition 12 (Model construction: Int and Elem variables). 1. Let A be a T LIA -interpretation with ApIntq " Z that satisfies A. Then Mpxq :" Apxq for every variable x of sort Int. 2. Let a 1 , a 2 , . . . be an enumeration of MpElemq, and let e 1 , . . . , e n be an enumeration of the equivalence classes of " S whose variables have sort Elem. Then, for every i P r1, ns and every variable x P e i , Mpxq :" a i .

Lemma 7.
If y « updatepx, i, zq P S, then Mp x q " Mp y q.
Proof. By congruence, we have that S |ù |y| « |updatepx, i, zq|, and by saturation of L-Intro and the definition of Ó, we know that S |ù |updatepx, i, zq| « |x|. Thus, S |ù |x| « |y|. By Assumption 1, S |ù x « y , so by saturation of S-Prop, we have A |ù x « y . It follows from Definition 12 that Ap x q " Ap y q, and thus, Mp x q « Mp y q.
We now turn to assigning values to variables of sort Seq. We will first associate a sequence value with every sequence equivalence class (we write Mpeq for the value associated with equivalence class e). Then, for each equivalence class e and for each x P e, we define Mpxq :" Mpeq. We start by defining lengths. Note that because every atomic variable is in an atomic equivalence class, Definition 13 assigns a length to every atomic variable. In what follows, we denote the length assigned to Mpeq in Definition 13 by e .
Next, we define model values for atomic variables. We start with equivalence classes that contain unit-terms.

Definition 14.
An equivalence class e of " S is called a unit equivalence class if unitpxq P e for some x.

Definition 15 (Model construction: atomic variables in unit equivalence classes).
For every atomic variable x such that x " S unitpyq for some y, we set Mprxsq to be a sequence of length 1 whose only element is set to Mpyq.
Next we turn to atomic equivalence classes that are not unit. We begin by defining a graph in order to keep track of constraints that originate from the update symbol. This definition is an adaptation of the weak equivalence graph from [10] to the context of sequences, where operations are richer. In particular, we take into account not only whether a constraint of the form y « updatepx, i, aq appears in S, but also whether x and y are atomic, and whether the interpretation already given to i in Definition 12 is within the range determined by the length assigned to x and y in Definition 13.
V is the set of atomic equivalence classes. E Ď VˆV is a set of unordered edges, and δ : E Ñ PpNq is a labeling function on edges, such that pe 1 , e 2 q P E and k P δppe 1 , e 2 qq iff there are x P e 1 and y P e 2 such that y « updatepx, i, zq P S or x « updatepy, i, zq P S, where Mpiq " k and 0 ď k ă Mp e1 q " Mp e2 q.
Definition 17 (Weak equivalence). Given a weak equivalence graph G " pV, E, δq, for each i P N, we define a binary relation " i over V as follows: e 1 " i e 2 iff there exists a path p between e 1 and e 2 in G, such that for each edge d in p, δpdqztiu ‰ H.
It is routine to verify that: Lemma 8. For each i P N, " i is an equivalence relation over the atomic equivalence classes of " S .
Notice that even though " i is defined using update-terms, every atomic equivalence class e satisfies e " i e, even if it has no update-terms.
Let " max eP" S e be the maximal sequence length assigned in Definition 13. Let a 1 1 , a 2 1 , . . . , a 1 , a 1 2 , . . . , a 2 , . . . be an enumeration of the elements in MpElemq that were not assigned to any variable of Elem sort. For each i P r0, q, let E i 1 , E i 2 , . . . , E i ni be an enumeration of the equivalence classes of " i .
By Lemma 8, we have: For every atomic equivalence class e of " S , and for each i P r0, e q, there exists some j such that e P E i j .

Definition 18 (Model construction: atomic variables in non-unit equivalence classes).
Let e be an atomic equivalence class of " S that is not a unit equivalence class. We set the ith element of Mpeq for every i P r0, e q as follows. By Lemma 9, there exists some j such that e P E i j . 1. If there are e 1 P E i j , s P e 1 , x, and y such that x " S nthps, yq and Mpyq " i, we set the ith element of Mpeq to be Mpxq. 2. Otherwise, the ith element of Mpeq is set to a i j .
Next, we set the interpretation of non-atomic variables of sort Seq.
Definition 19 (Model construction: non-atomic sequence variables). Let x be a non-atomic variable of sort Seq, and let y be its normal form. Mprxsq is set to be the concatenation of the interpretations of the variables in y (Mprxsq is the empty sequence if y is of size 0).
Finally, we define the interpretation of nth. Mpnthq is a function from MpSeqqM pIntq to MpElemq. Given a P MpSeqq and an integer i, if i is non-negative and smaller than the length of a, the value of Mpnthqpa, iq is fixed by the theory. The following definition assigns a value to Mpnthqpa, iq when i is out of bounds.
Definition 20 (Model construction: nth terms). For every element a P MpSeqq with length n and for every i P N such that i ă 0 or i ě n, if there are s, x, and y such that x " S nthps, yq, Mpsq " a, and Mpyq " i, Mpnthqpa, iq is set to Mpxq. Otherwise, it is set arbitrarily.
This concludes the construction of M. This lemma is proved in Appendix A.6, below. By construction, M is a T Seq -interpretation, and by Lemma 10 it is well-defined. It is left to show that it satisfies A Y S. The arithmetic constraints are satisfied, by the fact that A |ù A (see Definitions 11 and 12): Showing that M |ù S is more involved. Roughly speaking, each possible shape of a sequence constraint is considered separately, and for each, M is proved to satisfy constraints of that shape from S. The cases that include nth and update terms heavily rely on the construction of the weak equivalence graph. Constraints that include concatenation are handled by reasoning about |ù``.

Lemma 12. M satisfies S.
This lemma will be proved in Appendix A. 7. We conclude this section by reviewing the earlier example for the construction of M with a few more details.
Example 6. Consider a signature in which Elem is Int, and a saturated configuration pS˚, A˚q w.r.t. EXT that includes the following formulas: y « y 1`y2 , x « x 1`x2 , y 2 « x 2 , y 1 « updatepx 1 , i, aq, |y 1 | " |x 1 |, |y 2 | " |x 2 |, nthpy, iq « a, nthpy 1 , iq « a. Following the above construction, a satisfying interpretation M can be built as follows: Definition 10 Set both MpIntq and MpElemq to be the set of integer numbers. MpSeqq is fixed by the theory. Definition 12 First, find an arithmetic model, Mp x q " Mp y q " 4, Mp y1 q " Mp x1 q " 2, Mp y2 q " Mp x2 q " 2, Mpiq " 0. Further, set Mpaq " 0. Definition 13 Start assigning values to sequences. First, set the lengths of Mpxq and Mpyq to be 4, and the lengths of Mpx 1 q, Mpx 2 q, Mpy 1 q, Mpy 2 q to be 2. Definition 18 Definition 15 is skipped as there are no unit terms. Next, according to Item 1, the 0th element of Mpy 1 q is set to 0 (y 1 is atomic, y is not.). According to Item 2, assign fresh values to the remaining indices of atomic variables. The result can be, e.g., Mpy 1 q " r0, 2s, Mpx 1 q " r1, 2s, Mpy 2 q " Mpx 2 q " r3, 4s. Definition 19 Assign non-atomic sequence variables based on equivalent concatenations: Mpyq " r0, 2, 3, 4s, Mpxq " r1, 2, 3, 4s. Definition 20 No integer variable in the formula was assigned an out-of-bound value, and so the interpretation of nth on out-of-bounds cases is set arbitrarily. Note that Definitions 10 and 11 are trivially well-defined. We now go through the remaining definitions.
Lemma 13. Definition 12 is well-defined. Proof. To show that Item 1 is well-defined, it suffices to note that by saturation of A-Conf, A is T LIA -satisfiable. To show that Item 2 is well-defined, it suffices to establish an infinite enumeration a 1 , a 2 , . . . of MpElemq, which is guaranteed to exist due to Definition 10.

Lemma 14.
Definition 13 is well-defined. Proof. Let x, y P e. We show that Mp x q " Mp y q. Since x " S y, we have S |ù |x| « |y|. By Assumption 1, we also have S |ù x « y . By saturation of S-Prop, we have x « y P A, and hence, by Definition 12, Mp x q " Mp y q.
Lemma 15. Definition 15 is well-defined. Proof. We first show that rxs is 1. To see this, note first that by saturation of L-Intro (and Figure 3), we have S |ù |unitpyq| « 1. We also have x « |x| P S by Assumption 1. It follows that S |ù x « 1, so x « 1 P A by saturation of S-Prop. Thus, we must have Ap x q " 1 in Definition 12, and thus Mp x q " 1. By Definition 13, we then have that the length of Mprxsq must be 1.
Lemma 16. Definition 18 is well-defined. Proof. Let e be as in Definition 18. Suppose there are e 1 , e 2 P E i j , with s 1 P e 1 , s 2 P e 2 , and x 1 , y 1 , x 2 , y 2 such that x 1 " S nthps 1 , y 1 q and x 2 " S nthps 2 , y 2 q and Mpy 1 q " Mpy 2 q " i, with i P r0, e q. We prove that Mpx 1 q " Mpx 2 q.
We first show that y 1 « y 2 P S. Clearly y 1 , y 2 P T pSq. Also, y 1 , y 2 P T pAq since y 1 « y 1 P A and y 2 « y 2 P A by saturation of S-Prop. It follows by saturation of S-A that either y 1 « y 2 P A or y 1 ff y 2 P A. Since Mpy 1 q " Mpy 2 q, the latter cannot hold, and so the former holds. Then, by saturation of A-Prop, we have y 1 « y 2 P S as well. Now, notice that e 1 " i e 2 . Hence, there exist e 1 , . . . , e n such that e 1 " e 1 , e n " e 2 and for k P r1, nq, e k and e k`1 are connected by an edge d k in G where δpd k qztiu ‰ H. For every such k, we have that s k « updateps 1 k , y k , z k q P S or s 1 k « updateps k , y k , z k q P S for some s k P e k , s 1 k P e k`1 , integer variable y k , and Elem-variable z k . By Lemma 7, Mp s k q " Mp s 1 k q. And by Definition 13, e k " Mp s k q and e k`1 " Mp s 1 k q. It follows that e 1 " e1 " . . . " en " e 2 . By a similar argument, because e " i e 1 , we have e 1 " e . We also have: p˚q Mpy k q ‰ i and p˚˚q Mpy k q P r0, e q. Define s 1 0 to be an alias for s 1 and then notice that for k P r1, nq, s k " S s 1 k´1 because s k , s 1 k´1 are both in e k .
We prove by induction that for k P r0, nq, nthps 1 , y 1 q " S nthps 1 k , y 1 q. For the base case, we simply note that nthps 1 , y 1 q and nthps 1 0 , y 1 q are identical and nthps 1 , y 1 q P T pSq. For the induction step, suppose that nthps 1 , y 1 q " S nthps 1 k , y 1 q, where k P r0, n´1q. This implies nthps 1 k , y 1 q P T pSq, and we also know s 1 k " S s k`1 . Recalling that s k`1 « updateps 1 k`1 , y k`1 , z k`1 q P S or s 1 k`1 « updateps k`1 , y k`1 , z k`1 q P S, we see that the premises of Nth-Update are satisfied. By saturation of Nth-Update, then, there are three possibilities. 1. In the first case, A |ù y 1 ă 0 _ y 1 ě s 1 k . We know from Definition 12 that Mpy 1 q " Apy 1 q and Mp s 1 k q " Ap s 1 k q, so we must have Mpy 1 q ă 0 or Mpy 1 q ě Mp s 1 k q. But Mpy 1 q " i and i P r0, e q, and we know that Mp s 1 k q " e k`1 " e , so this case is not possible. 2. In the second case, A |ù y 1 « y k`1 . This is also not possible because we know that Apy 1 q " Mpy 1 q " i ‰ Mpy k`1 q " Apy k`1 q. 3. We are thus left with the third option, in which nthps k`1 , y 1 q " S nthps 1 k`1 , y 1 q. But we know that s 1 k " S s k`1 , so we also have nthps 1 k , y 1 q " S nthps 1 k`1 , y 1 q. Then, by the induction hypothesis, nthps 1 , y 1 q " S nthps 1 k`1 , y 1 q, which completes the induction proof. Letting k " n´1, we obtain nthps 1 , y 1 q " S nthps 1 n´1 , y 1 q. But s 1 n´1 P e n and e n " e 2 , so s 1 n´1 " S s 2 and nthps 1 , y 1 q " S nthps 2 , y 1 q. Finally, since we showed above that y 1 « y 2 P S, we have nthps 1 , y 1 q " S nthps 2 , y 2 q, and thus x 1 " S x 2 , which means that Mpx 1 q " Mpx 2 q by Definition 12.
Lemma 17. Definition 19 is well-defined. Proof. y exists and is unique by Lemma 4. If y is a variable or a variable-concatenation term, then uniqueness guarantees well-definedness. Further, each variable that occurs in y is atomic by Lemma 4, and hence its value in M was already defined in Definitions 15 and 18. We prove that Definition 20 is well-defined, but first we prove some helper lemmas. Recall that we write C |ù LIA ϕ to denote that every model of T LIA satisfying C also satisfies ϕ. Intuitively, if ϕ can be derived from C using arithmetic reasoning, then C |ù LIA ϕ.
Lemma 18. If S |ù``x « z and z is of size n, then A |ù LIA x " Σ n i"1 zi .
Proof. The proof is by structural induction using Definition 6. For Item 1, clearly A |ù x « x . For Item 2, we have S |ù``x « t for some variable concatenation term t " t 1`¨¨¨`tn such that S |ù x « t. Therefore, S |ù |x| « |t|. By saturation of L-Intro, S |ù |x| « Σ n i"1 |t i |, and using Assumption 1, we get S |ù x « Σ n i"1 ti . By saturation of S-Prop, A |ù x « Σ n i"1 ti . Now suppose that S |ù``x « pw``y``zqÓ and S |ù y « t, where t is or a variable concatenation term in T pSq. Let w " pw 1 , . . . , w m q and z " pz 1 , . . . , z n q, with m, n ě 0. By the induction hypothesis, we have that A |ù LIA x « Σ m i"1 wi` yΣ n i"1 zi . We consider two cases. (1) t " : in this case, S |ù |y| « | |. Also, S |ù | | " 0 by saturation of L-Intro, so S |ù |y| " 0, and thus A |ù y " 0 by saturation of S-Prop and Assumption 1. It follows that A |ù LIA x « Σ m i"1 wi`Σ n i"1 zi . (2) t is a variable concatenation term in T pSq: let t " t 1`. . .``t k . We have S |ù |y| « |t|. Also, S |ù |t| " Σ k i"1 |t i | by saturation of L-Intro. By saturation of S-Prop and Assumption 1 (and assuming wlog that Σ k i"1 ti is the result of flattening Σ k i"1 |t i |), it follows that A |ù y " Σ k i"1 ti . Thus, A |ù LIA x « Σ m i"1 wi`Σ k i"1 ti`Σ n i"1 zi .
Lemma 19. For every sequence variable x P S, if is the length of Mpxq, then Mp x q " .
Proof. If x is atomic, then " Mp x q by Definition 13. Suppose that x is non-atomic. Let y be the normal form of x where y is of size n. Each element of y is atomic, so for i P r1, ns, the length of Mpy i q is Mp yi q by Definition 13. Then, " Σ n i"1 Mp yi q by Definition 19. Let z of length n be such that S |ù``x « z and S |ù y i « z i for i P r1, ns, which exists by Definition 6. By Lemma 18, we have that A |ù LIA x « Σ n i"1 zi . For each i P r1, ns, we know that because S |ù y i « z i , S |ù |y i | « |z i |, and so by Assumption 1, S |ù yi « zi . Therefore, A |ù yi « zi by saturation of S-Prop. Then, we can conclude that A |ù LIA x « Σ n i"1 yi . Finally, we have Mp x q " Ap x q " Σ n i"1 Ap yi q " Σ n i"1 Mp yi q " .
case, we must have A |ù y ă 0 _ y ě x . But we also know that Mpyq " i is non-negative and is smaller than the length assigned to M pxq, which leads to a contradiction using Lemma 19. For the other cases, we have, for some k P r1, ns, (1) A |ù Σ k´1 j"1 yj ď y ă Σ k j"1 yj and (2) S |ù nthpx, yq « nthpy k , y´Σ k´1 j"1 yj q. By Definition 12, this means that Σ k´1 j"1 Mp yj q ď Mpyq ă Σ k j"1 Mp yj q. Now, by Definition 19, Mpxq " Mpy 1 q``¨¨¨``Mpy n q, and by Lemma 19, the length of Mpy j q is Mp yj q for j P r1, ns. Let i 1 " Mpyq´Σ k´1 j"1 Mp yj q. Clearly, i 1 P r0, Mp y k qq, and element Mpyq of Mpxq is the same as element i 1 of Mpy k q. Now, revisiting (2), let α be the term y´Σ k´1 j"1 yj , and letα be the variable introduced for α when flattening the term nthpy k , αq. We have k " S nthpx, yq, so k " S nthpy k ,αq by (2). Let i 2 be Mpαq, and recall that y k is atomic and that the length of Mpy k q is Mp y k q. By Lemma 20, we have that if i 2 P r0, Mp y k qq, then the i 2 th element of Mpy k q is Mpkq. It remains to show that i 1 " i 2 . To see this, note that S |ùα « α. So, by saturation of S-Prop, we have A |ùα « α. Then, by Definition 12, i 2 " Mpαq " Mpyq´Σ k´1 j"1 Mp yj q " i 1 .

Lemma 22.
For all x, y, with x ff y P S, we have Mpxq ‰ Mpyq.
Proof. By Deq-Ext we have two cases. In the first, A |ù x ‰ y . So, by Definition 12, Mp x q ‰ Mp y q. Thus, by Lemma 19, we have that the length of Mpxq is different from the length of Mpyq, so Mpxq ‰ Mpyq.
In the second case, we have (1) A |ù x « y^0 ď i ă x and (2) w 1 « nthpx, iq, w 2 « nthpy, iq, w 1 ff w 2 P S, for some i, w 1 , w 2 . By (2) and saturation of S-Conf, we know that w 1 ı S w 2 , so by Definition 12, Mpw 1 q ‰ Mpw 2 q. Let n " Mpiq and let be the length of Mpxq. By Definition 12, we have Mp x q " Mp y q and 0 ď n ă Mp x q. So, by Lemma 19, we have that the lengths of Mpxq and Mpyq are both equal to , and n P r0, q. Looking again at (2), we can apply Lemma 21 twice to get that the nth element of Mpxq is Mpw 1 q and the nth element of Mpyq is Mpw 2 q. We can then conclude that Mpxq ‰ Mpyq, as we know that Mpw 1 q ‰ Mpw 2 q.
We can now show that Definition 20 is well-defined.
Lemma 23. Definition 20 is well-defined. Proof. Suppose there are x, x 1 , s, s 1 , y, y 1 such that x " S nthps, yq, x 1 " S nthps 1 , y 1 q, Mpsq " Mps 1 q " a, and Mpyq " Mpy 1 q " i. We prove Mpxq " Mpx 1 q. Since y, y 1 P T pSq, and they have sort Int, by saturation of S-Prop, we have that y « y, y 1 « y 1 P A, and so y, y 1 P T pSq X T pAq. By saturation of S-A, either y ff y 1 P A or y « y 1 P A. The first case is impossible since Mpyq " Mpy 1 q. In the second case, we have y « y 1 P A, and so y « y 1 P S by saturation of A-Prop. Now, by saturation of Nth-Split, there are two options: either s ff s 1 P S or s « s 1 P S. The first is impossible by Lemma 22, as Mpsq " Mps 1 q. On the other hand, if s « s 1 P S, then since x " S nthps, yq and x 1 " S nthps 1 , y 1 q, we also have x " S x 1 . Thus, by Definition 12, we have Mpxq " Mpx 1 q. least 2. Now, by saturation of Update-Concat-Inv applied to z m « updatepw m , α m , vq, we have w m « z 1 P S, u 1 « updatepz 1 1 , α m , vq P S, and u 2 « updatepz 1 2 , α 1 , vq P S, for some α 1 where S |ù α 1 " α m´ u1 . By Lemma 7, we have Mp u1 q " Mp z 1 1 q and Mp u2 q « Mp z 1 2 q. But u 1 and u 2 are atomic, so by Lemma 26, their lengths cannot be zero. By Lemma 19, then, the lengths of z 1 1 and z 1 2 are also nonzero. So S * z 1 « and S * z 2 « by Lemma 26. Thus, z is not singular, which means that w m is not atomic, which is a contradiction. Now, consider the following n`2 constraints: i ă 0, ř k´1 j"1 wj ď i ă ř k j"1 wj for k P r1, ns, and i ě ř n j"1 wj . Exactly one of these holds in M, since it interprets arithmetic symbols in the usual way by Definition 11. Suppose M |ù i ă 0 or M |ù i ě ř n j"1 wj . We know that Mpiq P r0, Mp y qq, so this case is impossible by Lemmas 19 and 25. Now, suppose that M |ù ř k´1 j"1 wj ď i ă ř k j"1 wj for some k P r1, ns. Clearly, Item 2 holds for this k. We know that Update-Bound is saturated w.r.t. z m « updatepw m , α m , vq P S for m P r1, ns. Recall also that A |ù α m « i´ř m´1 j"1 wj . It is easy to see that the first branch is inconsistent with M whenever m ‰ k. Thus, we have z m « w m P S for m P r1, ns, m ‰ k.
Lemma 28. If x " S unitpyq then x is atomic.
Proof. Note that S |ù |unitpyq| « 1 by saturation of L-Intro, and so we also have (˚) S |ù |x| « 1. Assume x is not atomic. There are two cases. In the first case, x " S . But S |ù | | « 0 by saturation of L-Intro, so by (˚) and saturation of S-Prop, this implies A |ù 0 « 1, which contradicts saturation of A-Conf. In the second case, there exists a variable concatenation term x 1`¨¨¨`xn P T pSq such that S |ù x « x 1`¨¨¨`xn and x 1`¨¨¨`xn is not singular in S. By Lemma 5, we know that A |ù LIA Σ n i"1 xn ě 2. But by (˚) and saturation of S-Prop and L-Intro, together with Assumption 1, we also have A |ù Σ n i"1 xn " 1, which also contradicts saturation of A-Conf.
Definition 21. Define S |ù 1,3 x « t if there is a derivation of S |ù``x « t without using Item 2 of Definition 6.
Lemma 29. If S |ù˚`x « y, where y has size n, then for some z of size n such that z i " S y i , i P r1, ns, S |ù 1,3 x « z.
Proof. Since S |ù˚`x « y, there is some z 1 such that z 1 i " S y i , i P r1, ns and S |ù``x « z 1 . Consider the derivation tree described in Lemma 3, and let D be the path through the tree corresponding to the derivation of S |ù``x « z 1 . If D has no application of Item 2 of Definition 6, then the claim is proved by setting z to be z 1 . Otherwise, the first node in D must use Item 2 of Definition 6 to derive S |ù``x « t, where x « t P S. Suppose that t is not singular. Then, it is possible to derive S |ù 1,3 x « t by starting with S |ù 1,3 x « x and then applying Item 3 of Definition 6, using S |ù x « t. We can then replace the root of D with this derivation to get a derivation showing S |ù 1,3 x « z.
Suppose, on the other hand, that t is singular. Suppose t " t 1`. . .``t m . Without loss of generality, assume that D eagerly applies Item 3 of Definition 6 m´1 times, each time using S |ù t i « for some i P r1, ms, which is possible because t is singular.