Introduction

In many program languages, integer data types represent only a fixed number of values. A sequence of bits is utilized to represent an integer via two's complement or a binary encoding. We call such a sequence of bits a bit-vector. The SMT-LIB [1] theory of "FixedSizeBitVectors" 1 is well-suited for modeling such programming languages since it offers many function symbols that capture precisely the semantics operations that occur in programming languages.

However, the expressiveness of the bit-vector theory comes at a certain price. Due to their complex semantics, formulas of this theory are rather intractable and there are only few algorithms that handle these formulas directly. Typically, algorithms that work on bit-vector formulas first do a translation, either to propositional logic or to integer arithmetic. The translation to propositional logic is called bit-blasting [2,3]. Bit-blasting translates each bit of a bit-vector into a propositional logical variable and translates each bit-vector operation into a propositional logical formula that captures exactly the semantics of that operation. The strength of bit-blasting is that we can utilize powerful SAT solvers for deciding statisfiability of the resulting formulas. The alternative to bit-blasting is the translation to integer arithmetic. A recent publication coined the term int-blasting [4] for this translation. Here, bit-vector variables are translated to integer variables and a comprehensive application of modulo operations makes sure that we can establish a connection between models for the bit-vector formulas and models for the integer formulas. In order to model bit-precise bit-vector operations, int-blasting can access individual bits via a combination of integer division (div) and modulo (mod) operations. E.g., if we translate a bit-vector variable x into an integer variable x' such that x is the binary encoding of x', we can access the third least-significant bit as follows: We divide x' by 4 and take the result modulo two. The result is one iff this bit was set to true. In order to improve the performance, int-blasting-based translations often work with approximations and increase their precision later if required.

Even though the state of the art to decide the satisfiability of bit-vector formulas is bit-blasting [2], there exist applications that need a translation from bit-vector formulas to formulas over integers. For example in software model checking many techniques only work on integers: loop acceleration [5,6], invariant syntheses [7,8] and syntheses of ranking functions [9,10,11]. While other techniques perform better on integers, especially Craig interpolation.

In this paper we present a translation from bit-vectors to integers that is closely related to the translation of [4]. In order to explain our translation and conceptual differences to [4] we use the functions nat2bv 𝑘 and bv2nat (see Section 3) which implement the binary encoding of natural numbers and its inverse function, respectively. The translation of [4] ensures the following relation between models of bit-vector formulas and the models of the resulting integer formulas: If the bit-vector model maps a term 𝑡 to a bitvector value 𝑣 then the integer model maps the translation result of 𝑡 to bv2nat(𝑣). In order to ensure this relation, the translation of [4] adds constraints that require that integer variables are in a given range and modulo operations such that every integer term is in the same range as its corresponding bit-vector term.

Our translation only requires a less strict relation between models of bit-vector formulas and the models of the resulting integer formulas. If the integer model maps the translation result of the term 𝑡 to an integer 𝑣 ′ then the bit-vector model maps 𝑡 to nat2bv(𝑣 ′ ) . I.e., we do not require that nat2bv(𝑣 ′ ) is the binary encoding of 𝑣 ′ , we only require that nat2bv(𝑣 ′ ) is the binary encoding of nat2bv(𝑣 ′ mod 𝑘), where 𝑘 is the bit-length of 𝑡. This conceptual difference to [4] allows us to omit constraints on the translated variables and it allows us to omit several modulo operations that the translation of [4] introduces.

The translation of [4] introduces modulo operations after each arithmetic operation. Our translation omits modulo operations after arithmetic operations but introduces modulo operations before each operation where we need that integer values are in a certain range. E.g., we translate bvult to the less-than relation < but apply a modulo operation to both operands. We call the translation of [4] eager int-blasting and our translation lazy int-blasting. Example 1. For the bit-vector formula: (bvult 𝑦 (bvadd 0101 (bvmul 𝑦 0011))). The result of the eager int-blasting is:

(< 𝑦 ′ (mod (+ 5 (mod (• 𝑦 ′ 3) 2 4 )) 2 4 )) ∧ (≥ 𝑦 ′ 0) ∧ (< 𝑦 ′ 2 4

). The result of our lazy int-blasting is: (< (mod 𝑦 ′ 2 4 ) (mod (+ 5 (• 𝑦 ′ 3)) 2 4 )).

Technically, our translation proceeds in two steps. In the first step, we inductively translate the formula and distinguish two cases. If the SMT-LIB semantic definition of the operation that we have to translate utilizes the functions bv2nat and nat2bv 𝑘 , we replace the operation with their semantic definition. For most of the other operations our translation is similar to the eager int-blasting. The result of our first translation step contains the functions bv2nat and nat2bv 𝑘 only as a concatenation bv2nat∘nat2bv 𝑘 . Our second translation step replaces this concatenation either by a modulo operation or by the identity function.

An additional contribution of this paper is that we present how we translate quantified formulas and arrays over bit-vectors into integers.

We have implemented our translation in two ways: as a wrapper script [12] for SMT solver and directly in the SMT solver SMTInterpol [13]. Through our evaluation of both implementations, we demonstrated that our translation does not produce incorrect results on the benchmark set. Moreover, we conducted a comparison between two settings of our translation implemented in SMTInterpol: one setting adds modulo operations lazily, while the other adds them eagerly. Our evaluation results revealed that SMTInterpol is capable of solving 9% more tasks, is 10% faster, and requires 23% less memory when modulo operations are added lazily compared to eagerly.

Related Work

There have been numerous approaches to translating from bit-vectors to integers. Some methods perform the translation during the verification process e.g. on the source level [14] or during invariant synthesis [15]. More closely related to our work are translations for SMT formulas [16,17,18,19,4]. However, our translation approach differs from the related work. Firstly, we incorporate modular arithmetic lazily to eliminate redundant modulo operations in the translation result. There exist simplification techniques to eliminate such redundant modulo operations. For example when the SMT solver Z3 is asked simplify(mod (• (mod (+ 𝑥 𝑦) 256) 𝑧) 256), it returns (mod (• 𝑧 (+ 𝑥 𝑦)) 256). However, since we do not add the redundant modulo operations in the first place, there is no need for such a simplification on our translation results. Secondly, no other approach utilizes function symbols with behavior similar to the functions bv2nat and nat2bv 𝑘 . We give a brief overview of the related approaches.

A similar concept to our lazy translation, but in a different research field, can be found in [20]. Where the authors apply modulo operations lazily during their translation from BTOR to C. Their evaluation shows that their lazy translation is faster in general, but not strictly better than their eager translation.

Griggio et al. introduces a layered SMT solver in [16], where on the higher layers, the solver performs translation from bit-vector formulas to integer formulas. This translation is for a fragment of the bit-vector functions, including arithmetic functions, extraction, concatenation, left shift, and relations. Rather than incorporating modulo operations to bound the integers, Griggio's approach utilizes an auxiliary variable, such as variable 𝑣 in the expression

(𝑡 1 + 𝑡 2 − 2 𝑛 • 𝑣) ∧ (0 ≤ 𝑣) ∧ (𝑣 ≤ 1)

. Each integer term derived during the translation is within the bounds of its corresponding bit-vector term, effectively achieving an eager translation.

Backeman, Rummer, and Zeljic [18] introduce a new calculus for non-linear integer arithmetic, which, in certain cases, can eliminate quantifiers and extract Craig interpolants. Subsequently, they define a corresponding calculus for arithmetic bit-vector constraints. Both calculi allow for a flexible switch between bit-vectors and integers. Initially, integers are not bound by modular arithmetic; instead, the authors introduce an uninterpreted function symbol that represents the modulo operation. They note that the remainder operation tends to be a bottleneck for interpolation. If necessary, a definition for the uninterpreted function symbol can be added to precisely cover the remainder. In contrast to our approach with uninterpreted function symbols, their uninterpreted function is directly associated with the modulo operation and does not affect the sort of a term. Furthermore, their approach supports a translation of quantified formulas, but not of arrays over bit-vectors.

Recently, the first precise and complete translation for bit-vector formulas with bit-vectors of fixed size was published in [4]. This work is closely related to their translation for bit-vectors with parametric bit-width, proposed in their previous work [19]. The precise translation presented in [4] has been implemented in the cvc5 prover [21]. It employs a translation from bit-vector formulas to non-linear integer arithmetic formulas with uninterpreted functions and universal quantification. During the translation, modulo operations are added eagerly and without the use of uninterpreted function symbols. Our translation approach combines elements from the translation in [4] with the semantics of the theory of "FixedSizeBitVectors" defined in the SMT-LIB [1].

Preliminaries and Notations

The SMT-LIB [1] defines a many-sorted first-order logic with equality. In this paper we use the sorts, signatures Σ and theories defined in the SMT-LIB. In particular we use the sorts, signatures and theories of Booleans, fixed-size bit-vectors, integers, and arrays.

Bit-Vectors

The SMT-LIB defines a signature Σ Bv and a theory called "FixedSizeBitVectors" for bit-vectors of fixed size. For every possible bit-vector size 𝑘, that is every positive integer greater than zero, Σ Bv contains a unique sort 𝜎 𝑘 . We call a term of sort 𝜎 𝑘 ∈ Σ Bv bit-vector of size 𝑘 or bit-vector of width 𝑘. In the following let 𝑥 be a bit-vector variable, 𝑐 be a bit-vector constant, and 𝑡, 𝑡 1 , and 𝑡 2 be bit-vector terms. Furthermore, let the width of bit-vectors 𝑥, 𝑐 and 𝑡 be 𝑘, the width of 𝑡 1 be 𝑘 1 and the width of 𝑡 2 be 𝑘 2 . The signature Σ Bv as defined in the SMT-LIB contains a set of bit-vector function symbols. We denote the extract function from 𝑖 to 𝑗 as extract 𝑖 𝑗 (𝑡), where 𝑖 and 𝑗 are natural numbers with 𝑖, 𝑗 ≥ 0 ∧ 𝑖 ≥ 𝑗. For the other bit-vector functions 𝑓 we use the notation 𝑓 (𝑡 1 𝑡 2 ) instead of the SMT-LIB notation (𝑓 𝑡 1 𝑡 2 ).

Integers

The SMT-LIB defines a signature Σ Int and a Σ Int -theory for mathematical integers. The sort 𝜎 ∈ Σ Int is defined as the set of all integers. The integer signature Σ Int consists of variables, constants and the usual functions and relations. Let constants 𝑐 ′ and terms 𝑡 ′ , 𝑡 ′ 1 and 𝑡 ′ 2 all have sort Int. As notation for integer functions we write

(𝑡 ′ 1 + 𝑡 ′ 2 ) instead of the SMT-LIB notation (+ 𝑡 ′ 1 𝑡 ′ 2 )

. In [4] the authors introduce a binary function symbols & 𝑘 (−, −), for every positive integer 𝑘. The functions & 𝑘 (−, −) are introduced to represents bit-wise and. Therefore, they extend the signature Σ Int and define two theories for this extended signature. We will do the same in this paper and refer to [4] for details.

Functions bv2nat and nat2bv 𝑘

In the theory of "FixedSizeBitVectors" the functions bv2nat and nat2bv 𝑘 are defined. Given an arbitrary binary 𝑏 = (𝑏 𝑘−1 , ..., 𝑏 𝑖 , ..., 𝑏 0 ) and its corresponding natural number 𝑛, the function bv2nat is defined as follows: bv2nat(𝑏) := ∑︀ 𝑘−1 𝑖=0 𝑏 𝑖 • 2 𝑖 . Furthermore, the function nat2bv 𝑘 is defined as: nat2bv 𝑘 (𝑛) := (𝑏 𝑘−1 , ..., 𝑏 𝑖 , ..., 𝑏 0 ), where 𝑏 𝑖 = 𝑛 div 2 𝑖 mod 2.

Note, we do not extend our signatures and theories with bv2nat and nat2bv 𝑘 . Instead, we treat them as auxiliary functions and ensure they are eliminated in the translation result. For the sake of readability, we denote bv2nat(𝑡) and nat2bv 𝑘 (𝑡 ′ ) as 𝑡 bv2nat and 𝑡 ′nat2bv 𝑘 , respectively.

Translation with bv2nat and nat2bv 𝑘

Our bit-vector to integer translation maps from the set of Σ Bv -formulas to the set of Σ Int -formulas (extended with & 𝑘 (−, −)). We say a translation "translates" a term or formula if it associates that term or formula with an element of its co-domain. Before we can define the translation, we need to define some auxiliary functions. First we define a variable mapping 𝜒. Similar to the variable mapping defined in [4], 𝜒 maps a variable of sort bit-vector to a fresh variable of sort integer. We extend the definition of 𝜒 for arrays over bit-vectors and quantified variables. Definition 4.1 (Variable Mapping 𝜒). Given a bit-vector formula 𝜑, we define a one-to-one mapping 𝜒 as the following. For every variable and quantified variable 𝑥 that occurs in 𝜑, 𝜒 maps to a fresh variable 𝑥 ′ , such that if 𝑥 is of sort Bv, then 𝑥 ′ is of sort Int. If 𝑥 is of sort Array with arguments of sort 𝑠 ∈ {Bv, Array} then 𝑥 ′ is of sort Array with arguments of sort 𝑠 ′ ∈ {Int, Array} correspondingly. Finally, if 𝑥 is of sort Bool, then 𝑥 ′ is of sort Bool. We write 𝜒 maps 𝑥 to 𝑥 ′ as 𝜒(𝑥) = 𝑥 ′ .

In Table 1 we use the auxiliary function 𝑢𝑡𝑠 𝑘 (−) from [4]. For a bit-vector term 𝑡 ′ , 𝑢𝑡𝑠 𝑘 (𝑡 ′ ) is an abbreviation for the term 2 • (𝑡 ′ mod 2 𝑘−1 ), which transforms an unsigned bit-vector to a signed bit-vector. Initially, our translation interprets every bit-vector as unsigned. In the case of a signed relation, we enclose the arguments of the relation with the function 𝑢𝑡𝑠 𝑘 . to ensures that the semantics of signed relation is preserved properly.

Finally, we define the translation function 𝑇 that maps from Σ Bv -formulas 𝜑 of the theory of bitvectors to Σ Int -formulas 𝜓 of the theory of integers (extended with & 𝑘 (−, −)). Therefore, we define a conversion functions 𝐶 in Table 1 (column Lazy) and a replacement function 𝑅 in Table 3. The translation function 𝑇 is defined as:

𝑇 := 𝜑 ↦ → 𝑅(𝐶(𝜑))

Our translation consist of two steps. In step one 𝐶 replaces bit-vector formulas and terms by their semantic definition. The conversion functions 𝐶 matches a term or formula 𝑒 to a term or formula in the first column. The match is then translated to the term or formula in the middle column named Lazy. For a direct comparison, we display the translation steps from the Eager translation in [4] in the third column in gray. Note, in [4] the authors translate a bit-vector variable 𝑣 by adding constraints in the form of (0 ≤ 𝜒(𝑣) < 2 𝑘 ) to the translation result and do not surround the integer variable 𝜒(𝑣) with modulo as we do in the third column of Table 2. For readability reasons, we split the definition of function 𝐶 into three functions: 𝐶, 𝐶 𝑡 and 𝐶 ′ 𝑡 . Functions 𝐶 𝑡 and 𝐶 ′ 𝑡 are both defined in Table 2. The conversion function uses bv2nat and nat2bv 𝑘 to replace bit-vector formulas and terms by their semantic definition, but our signature Σ Int and integer theory do not contain bv2nat and nat2bv 𝑘 . In the second step, we use the replacement function 𝑅 to get rid of bv2nat and nat2bv 𝑘 . Therefore, we either remove the concatenation bv2nat ∘ nat2bv 𝑘 or replace it with a modulo operation. In the tables defining 𝐶, 𝐶 𝑡 , and 𝐶 ′ 𝑡 , we have indicated certain bv2nat function calls in blue. If function 𝑅(𝑒) matches 𝑒 to (𝑡 ′nat2bv 𝑘 ) bv2nat where bv2nat is marked blue, then we replace 𝑒 with 𝑡 ′ mod 2 𝑘 . Otherwise, if bv2nat is not marked blue we replace (𝑡 ′nat2bv 𝑘 ) bv2nat with 𝑡 ′ .

So far we translate bvand to the uninterpreted function symbol & 𝑘 (−, −) in 𝐶 and do not treat it any further. For a more sophisticated translation of bvand we refer to literature [4].

Lazy Eager

𝐶(𝑒) :

𝑀 𝑎𝑡𝑐ℎ 𝑒 :

𝑡 1 = 𝑡 2 𝐶 𝑡 (𝑡 1 ) bv2nat = 𝐶 𝑡 (𝑡 2 ) bv2nat 𝐶 𝑡 (𝑡 1 ) = 𝐶 𝑡 (𝑡 2 ) bvult(𝑡 1 , 𝑡 2 ) 𝐶 𝑡 (𝑡 1 ) bv2nat < 𝐶 𝑡 (𝑡 2 ) bv2nat 𝐶 𝑡 (𝑡 1 ) < 𝐶 𝑡 (𝑡 2 ) bvule(𝑡 1 , 𝑡 2 ) 𝐶 𝑡 (𝑡 1 ) bv2nat ≤ 𝐶 𝑡 (𝑡 2 ) bv2nat 𝐶 𝑡 (𝑡 1 ) ≤ 𝐶 𝑡 (𝑡 2 ) bvslt(𝑡 1 , 𝑡 2 ) 𝑢𝑡𝑠 𝑘 (𝐶 𝑡 (𝑡 1 ) bv2nat ) < 𝑢𝑡𝑠 𝑘 (𝐶 𝑡 (𝑡 2 ) bv2nat ) 𝑢𝑡𝑠 𝑘 (𝐶 𝑡 (𝑡 1 )) < 𝑢𝑡𝑠 𝑘 𝐶 𝑡 (𝑡 2 )) bvsle(𝑡 1 , 𝑡 2 ) 𝑢𝑡𝑠 𝑘 (𝐶 𝑡 (𝑡 1 ) bv2nat ) ≤ 𝑢𝑡𝑠 𝑘 (𝐶 𝑡 (𝑡 2 ) bv2nat ) 𝑢𝑡𝑠 𝑘 (𝐶 𝑡 (𝑡 1 )) ≤ 𝑢𝑡𝑠 𝑘 𝐶 𝑡 (𝑡 2 )) □(𝑡 1 , ...𝑡 𝑖 ) □(𝐶(𝑡 1 ), ..., 𝐶(𝑡 𝑖 )) □ ∈ {∧, ∨, ¬, ⇒, ⇔} 𝑢𝑡𝑠 𝑘 (𝑡 ′ ) := 2 • (𝑡 ′ mod 2 𝑘−1 ) − 𝑡 ′

Table 1

Definition of the Conversion Function 𝐶

Translation of Arrays and Quantified Formulas

For the translation of quantified formulas and arrays we extend our conversion functions 𝐶 and 𝐶 𝑡 with the conversions outlined in Table 4. Therefore, let in Table 4 𝑎 and 𝑏 be arrays over bit-vectors, where the bit-vectors that represent the indices of 𝑎 and 𝑏 have width 𝑘. Additionally, let 𝑖 ′ be a quantified integer variable. The translation of quantified formulas utilizes the variable mapping 𝜒(𝑣) = 𝑣 ′ , where 𝑣 is a quantified bit-vector variable of width 𝑘 and 𝑣 ′ is a quantified integer variable. Additionally, we ensure that a translated quantified formula is unsatisfiable for values of 𝑣 ′ that are not within the bounds of 𝑣. Therefore, we add the bound (0 ≤ 𝜒(𝑣) < 2 𝑘 ) as constraints within the scope of the quantifier.

Arrays over bit-vectors 𝑎 are translated to fresh arrays over integers with the help of the one-to-one mapping 𝜒(𝑎). Since arrays over integers have infinitely indices and arrays over bit-vectors don't, we have to add some limitations. First of all, we ensure to only read from and write to indices that are within the bounds of the corresponding bit-vector array. Secondly, we have to ensure that if two translated arrays are equal on every index in the range of the bit-vector array, then they are equal on every index. Therefore, we add a constraint to the translation result that evaluates to false if this condition is violated. This is achieved by the constraint function Lem in Table 4. Furthermore, we change the translation function to add constraints for every array equality:

𝑇 𝐴𝑟𝑟𝑎𝑦 := 𝜑 ↦ → 𝑅(𝐶(𝜑)) ∧ Lem(𝜑). Lazy Eager 𝐶 𝑡 (𝑒) : 𝑀 𝑎𝑡𝑐ℎ 𝑒 : concat(𝑡 1 , 𝑡 2 ) 𝐶 ′ 𝑡 (𝑒) nat2bv 𝑘 1 +𝑘 2 𝐶 ′ 𝑡 (𝑒) extract 𝑖 𝑗 (𝑡 1 ) 𝐶 ′ 𝑡 (𝑒) nat2bv𝑖−𝑗+1 𝐶 ′ 𝑡 (𝑒) else: 𝑒 𝐶 ′ 𝑡 (𝑒) nat2bv 𝑘 𝐶 ′ 𝑡 (𝑒) 𝐶 ′ 𝑡 (𝑒) : 𝑀 𝑎𝑡𝑐ℎ 𝑒 : 𝑥 𝜒(𝑥) 𝜒(𝑥) mod 2 𝑘 𝑐 ∑︀ 𝑘−1 𝑖=0 𝑐 𝑖 • 2 𝑖 where 𝑐 𝑖 is the 𝑖-th bit of 𝑐 bvneg(𝑡 1 ) 2 𝑘1 − 𝐶 𝑡 (𝑡 1 ) bv2nat 2 𝑘1 − 𝐶 𝑡 (𝑡 1 ) bvmul(𝑡 1 , 𝑡 2 ) 𝐶 𝑡 (𝑡 1 ) bv2nat • 𝐶 𝑡 (𝑡 2 ) bv2nat (𝐶 𝑡 (𝑡 1 ) • 𝐶 𝑡 (𝑡 2 )) mod 2 𝑘 bvadd(𝑡 1 , 𝑡 2 ) 𝐶 𝑡 (𝑡 1 ) bv2nat + 𝐶 𝑡 (𝑡 2 ) bv2nat (𝐶 𝑡 (𝑡 1 ) + 𝐶 𝑡 (𝑡 2 )) mod 2 𝑘 bvsub(𝑡 1 , 𝑡 2 ) 𝐶 𝑡 (𝑡 1 ) bv2nat − 𝐶 𝑡 (𝑡 2 ) bv2nat (𝐶 𝑡 (𝑡 1 ) − 𝐶 𝑡 (𝑡 2 )) mod 2 𝑘 bvudiv(𝑡 1 , 𝑡 2 ) ite(𝐶 𝑡 (𝑡 2 ) bv2nat = 0, 2 𝑘 − 1, 𝐶 𝑡 (𝑡 1 ) bv2nat div 𝐶 𝑡 (𝑡 2 ) bv2nat ) ite(𝐶 𝑡 (𝑡 2 ) = 0, 2 𝑘 − 1, 𝐶 𝑡 (𝑡 1 ) div 𝐶 𝑡 (𝑡 2 )) bvurem(𝑡 1 , 𝑡 2 ) ite(𝐶 𝑡 (𝑡 2 ) bv2nat = 0, 𝑡 1 , 𝐶 𝑡 (𝑡 1 ) bv2nat mod 𝐶 𝑡 (𝑡 2 ) bv2nat ) ite(𝐶 𝑡 (𝑡 2 ) = 0, 𝐶 𝑡 (𝑡 1 ), 𝐶 𝑡 (𝑡 1 ) mod 𝐶 𝑡 (𝑡 2 )) bvshl(𝑡 1 , 𝑡 2 ) ite(𝐶 𝑡 (𝑡 2 ) bv2nat = 1, 2 • 𝐶 𝑡 (𝑡 1 ) bv2nat , ... ite(𝐶 𝑡 (𝑡 2 ) bv2nat = 𝑘 − 1, 2 𝑘−1 • 𝐶 𝑡 (𝑡 1 ) bv2nat , 0)...) ite(𝐶 𝑡 (𝑡 2 ) = 1, 2 • 𝐶 𝑡 (𝑡 1 ) mod 2 𝑘 , ... ite(𝐶 𝑡 (𝑡 2 ) = 𝑘 − 1, 2 𝑘−1 • 𝐶 𝑡 (𝑡 1 ) mod 2 𝑘 , 0)...) bvlshr(𝑡 1 , 𝑡 2 ) ite(𝐶 𝑡 (𝑡 2 ) bv2nat = 1, 𝐶 𝑡 (𝑡 1 ) bv2nat div 2, ... ite(𝐶 𝑡 (𝑡 2 ) bv2nat = 𝑘 − 1, (𝐶 𝑡 (𝑡 1 ) bv2nat div 2 𝑘−1 ), 0)...) ite(𝐶 𝑡 (𝑡 2 ) = 1, 𝐶 𝑡 (𝑡 1 ) div 2, ... ite((𝐶 𝑡 (𝑡 2 ) = 𝑘 − 1), 𝐶 𝑡 (𝑡 1 ) div 2 𝑘−1 , 0)...) concat(𝑡 1 , 𝑡 2 ) 𝐶 𝑡 (𝑡 1 ) bv2nat • 2 𝑘2 + 𝐶 𝑡 (𝑡 2 ) bv2nat 𝐶 𝑡 (𝑡 1 ) • 2 𝑘2 + 𝐶 𝑡 (𝑡 2 ) extract 𝑖 𝑗 (𝑡 1 ) 𝐶 𝑡 (𝑡 1 ) bv2nat div 2 𝑗 𝐶 𝑡 (𝑡 1 ) div 2 𝑗 mod 2 𝑖−𝑗+1 bvnot(𝑡 1 ) 2 𝑘1 − 𝐶 𝑡 (𝑡 1 ) bv2nat + 1 2 𝑘1 − 𝐶 𝑡 (𝑡 1 ) + 1 bvand(𝑡 1 , 𝑡 2 ) & 𝑘 (𝐶 𝑡 (𝑡 1 ) bv2nat , 𝐶 𝑡 (𝑡 2 ) bv2nat ) & 𝑘 (𝐶 𝑡 (𝑡 1 ), 𝐶 𝑡 (𝑡 2 ))(𝑡 ′nat2bv 𝑘 ) bv2nat → 𝑅(𝑡 ′ ) otherwise else: 𝑒(𝑡 ′ 1 , ..., 𝑡 ′ 𝑛 ) → 𝑒(𝑅(𝑡 ′ 𝑖 ), ..., 𝑅(𝑡 ′ 𝑛 ))∧ (0 ≤ 𝜒(𝑣) < 2 𝑘 )) ∀ 𝑣.(𝑒) ∀ 𝐶(𝑣).((0 ≤ 𝜒(𝑣) < 2 𝑘 ) ⇒ 𝐶(𝑒)) 𝐶 𝑡 (𝑒) : 𝑀 𝑎𝑡𝑐ℎ 𝑒 : 𝑎 𝜒(𝑎) (select 𝑎 𝑖) (select 𝐶 𝑡 (𝑎) 𝐶 𝑡 (𝑖) bv2nat ) (store 𝑎 𝑖 𝑣) (store 𝐶 𝑡 (𝑎) 𝐶 𝑡 (𝑖) bv2nat 𝐶 𝑡 (𝑣)) Lem(𝑒) : 𝑀 𝑎𝑡𝑐ℎ 𝑒 : 𝑎 = 𝑏 (∀𝑖 ′ .(0 ≤ 𝑖 ′ < 2 𝑘 ) ⇒ ((select 𝐶 𝑡 (𝑎) 𝑖 ′ ) mod 2 𝑘 = (select 𝐶 𝑡 (𝑏) 𝑖 ′ ) mod 2 𝑘 )) ⇒ 𝐶 𝑡 (𝑎) = 𝐶 𝑡 (𝑏) □(𝑡 1 , ...𝑡 𝑖 ) ⋀︀ 𝑛 𝑖=1 Lem(𝑡 𝑖 ) □ ∈ {∧, ∨, ¬, ⇒, ⇔} else: ⊤ Table 4

Extension for Quantified Formulas and Arrays

Implementation

We have two implementations for our lazy translation presented in Section 4. The first implementation is a wrapper script for SMT solvers, called Ultimate IntBlastingWrapper [12]. It is implemented in the Ultimate framework 2 . The wrapper script does not use the functions bv2nat and nat2bv 𝑘 instead modulo operations are added directly. It supports a translation of bit-wise operations with all features described in [4], quantified formulas and arrays over bit-vectors.

The second implementation is in the SMT solver SMTInterpol 3 . This implementation is still work in progress. So far we use bv2nat and nat2bv 𝑘 as uninterpreted functions, but the implementation does not support bit-wise operations, quantified variables and arrays yet. We implemented two settings to translate bit-vectors to integers. The first setting is called Lazy and it applies our lazy translation in Section 4. The second setting is called Eager and it applies a translation similar to [4]. Each setting applies the conversions in their respective column in Table 2. Additionally, we compare our settings Lazy and Eager with the original implementation (cvc5-int) of [4] in the SMT solver cvc5. We selected SMTInterpol as the SMT solver for our evaluation because, at the point of writing, it did not support bit-vectors, and we were already familiar with the tool. Unfortunately, it did not support non-linear integer arithmetic either. When SMTInterpol encounters a bit-wise operation or non-linear integer arithmetic we return an error.

Evaluation

We evaluate our two implementations to answer the following research questions:

• How does the performance of the approach Lazy and Eager compare? • How does Lazy and Eager compare to int-blasting in cvc5?

Evaluation of Ultimate IntBlastingWrapper

We participated with Ultimate IntBlastingWrapper [12] at the latest SMT-COMP 2023. Ultimate IntBlastingWrapper competed in the Single Query Track on every logic that contains bit-2 https://ultimate.informatik.uni-freiburg.de and github.com/ultimate-pa/ultimate 3 https://github.com/ultimate-pa/smtinterpol/tree/Intblasting vectors. The results of Ultimate IntBlastingWrapper in the SMT-COMP 2023 showed wrong results on three benchmarks. Of these three, two are from the category QF_AUFBV and one from QF_ABV. The wrong results were caused by a mistake in the translation of equalities between arrays over bit-vectors. This has been fixed in commit: https://github.com/ultimate-pa/ultimate/commit/ 928447c7dc8c44e406f0a52121ccf96fcbe4d5b5.

Evaluation of Int-blasting in SMTInterpol

To evaluate our implementation in the SMTInterpol, we ran the settings Lazy and Eager and the implementation of int-blasting in cvc5 (cvc5-int) from the paper [4]. For cvc5-int we used the cvc5 options --solve-bv-as-int=sum and --nl-ext-tplanes. We run Lazy, Eager and cvc5-int on a randomly picked subset of the non-incremental QF_BV benchmarks from the SMT-LIB. From the set we excluded every benchmark where the expected result is unknown. There remained 12302 benchmarks.

Environment

We run our experiments on a cluster of machines with 33 GB of memory and an Intel Xeon E3-1230 v5 CPU with 8 processing units and a frequency of 3.40 GHz that run Ubuntu 22.04 (Linux kernel 5.15.0). To measure and limit resources we use Benchexec 3.18 [22]. We limit every run to 1 core, 15 min of CPU time and 15 GB of memory.

How does the performance of the approach Lazy and Eager compare? The evaluation results of Lazy and Eager are displayed in Table 5. We can see that SMTInterpol solves more benchmarks with Lazy than with Eager. Lazy creates 282 more correct results that is 9% (2698 of 2961). Among these, Eager times out on 280 cases, and on 2 cases, Eager reports that the formula contains non-linear integer arithmetic. On the other hand Eager returns a correct result on Eager times out. All errors in Table 5 are caused by either non-linear integer arithmetic or a bit-wise operation. To compare the CPU time and memory usage of Lazy and Eager, we analyze the 2679 benchmarks for which both settings return a correct result (see Table 6). When measuring the CPU time and memory used on these 2679 benchmarks, Lazy requires 10% less CPU time (23000 s out of 25600 s) and 23% less memory (252 GB out of 327 GB) to decide their satisfiability. For a more detailed view, we provide two scatter plots in Figure 1. Both scatter plots have logarithmic scales, the first shows the CPU time used and the second plot shows the memory usage. Every dot in the scatter plots below the line is in favor of Lazy. We observe that in many cases, the Lazy approach requires less CPU time and/or memory. Specifically, the CPU time and memory usage of Lazy tends to deviate less frequently and significantly from Eager. However, it is important to note that Lazy is not strictly superior to Eager.

How does Lazy and Eager compare to int-blasting in cvc5?

In Table 5, we observe that cvc5-int solves 8409 tasks. Out of these 8409 tasks Lazy times out on 553, returns an error on 5166 and solves correctly 2690. On the 2961 tasks where Lazy returns a correct result, cvc5-int times out 271 times and returns 2691 correct results. Among the 2006 benchmarks where Lazy, Eager, and cvc5-int all return a correct result, cvc5-int demonstrates significantly lower CPU time and memory usage. For solving these 2006 tasks, Lazy requires 30380 s, Eager requires 62800 s, and cvc5-int requires 12750 s. Regarding memory usage, Lazy consumes 246.7 GB, Eager consumes 321.4 GB, and cvc5-int consumes 16.5 GB.

The comparison between cvc5-int and our implementations shows that cvc5-int solves significantly more benchmarks. However, cvc5-int is not strictly superior, we solve 271 benchmarks on which cvc5-int times out.

Conclusion

We present a lazy translation from bit-vector formulas to integer formulas that utilizes the functions bv2nat and nat2bv 𝑘 . Our translation consists of a conversion function 𝐶, and a replacement function 𝑅. Conversion function 𝐶 replaces bit-vector terms and formulas with their semantic definition, thus incorporating bv2nat and nat2bv 𝑘 into the translation process This makes our translation more modular since bit-vector terms and their semantic definition have the same sort. Additionally, conversion function 𝐶 supports a translation of quantified formulas and arrays over bit-vectors. Within replacement function 𝑅, we eliminate bv2nat and nat2bv 𝑘 from the translation result and introduce modulo operations instead. This is done in such a way that the amount of redundant modulo operations is reduced. We implemented our lazy translation in the SMTInterpol and as wrapper script for SMT solver. Our evaluation of both implementations indicates the correctness of the lazy translation. Furthermore, it shows that SMTInterpol with our lazy translation is able to solve 9% more tasks, 10% faster and with 23% less memory usage than with a closely related, up-to-date eager translation approach.