In this paper we present a translation from bit-vector formulas to integer formulas. The translation uses the function symbols bv2nat and nat2bv which are both utilized in the theory of fixed-width bit-vectors of the SMT-LIB [1] language to define the semantics of bit-vector operations. Our translation replaces bit-vector operations with their semantic definition. This facilitates a more modular application as bit-vector operations and their semantic definition have the same sort. As a postprocessing our translation replaces the composition bv2nat ∘ nat2bv with a modulo operation, and removes redundant modulo operations from the translation result. The evaluation of our translation shows that we are able to solve 9% more tasks, 10% faster and with 23% less memory usage compared to a closely related, up-to-date translation approach. Additionally, our translation supports the translation of quantified formulas and arrays over bit-vectors.
Even though the state of the art to decide the satisfiability of bit-vector formulas is bit-blasting [
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 diferences 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 diference 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) 24)) 24)) ∧ (≥ ′ 0) ∧ (< ′ 24). The result of our lazy int-blasting is: (< (mod ′ 24) (mod (+ 5 (· ′ 3)) 24)).
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.
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 difers 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 diferent 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, efectively 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 afect 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 [
The SMT-LIB [
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).
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() := ∑︀=−01 · 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. 4. 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]. () : ℎ : 1 = 2 bvult(1, 2) bvule(1, 2) bvslt(1, 2) bvsle(1, 2) □ (1, ...)
Lazy
Eager (1)bv2nat = (2)bv2nat (1)bv2nat < (2)bv2nat (1)bv2nat ≤ (2)bv2nat ((1)bv2nat) < ((2)bv2nat) ((1)bv2nat) ≤ ((2)bv2nat) (1) = (2) (1) < (2) (1) ≤ (2) ((1)) < (2)) ((1)) ≤ (2)) □ ((1), ..., ()) □ ∈ {∧, ∨, ¬, ⇒, ⇔} (′) := 2 · (′ mod 2− 1) − ′
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(). ∑︀=−01 · 2 where is the -th bit of () : ℎ : concat(1, 2) ′()nat2bv1+2 extract(1) ′()nat2bv− +1 else: ′()nat2bv ′() : ℎ :
() bvneg(1) 21 − (1)bv2nat bvmul(1, 2) (1)bv2nat · (2)bv2nat bvadd(1, 2) (1)bv2nat + (2)bv2nat bvsub(1, 2) (1)bv2nat − (2)bv2nat bvudiv(1, 2) it(e(1)bv(2n2a)tbvd2inavt =(0,2)2bv2− nat1),
ite((2)bv2nat = 0, 1, bvurem(1, 2) (1)bv2nat mod (2)bv2nat) ite((2)bv2nat = 1, 2 · (1)bv2nat, bvshl(1, 2) ...
ite((2)bv2nat = − 1, 2− 1 · (1)bv2nat, 0)...) ite((2)bv2nat = 1, (1)bv2natdiv 2, bvlshr(1, 2) ...
ite((2)bv2nat = − 1, ((1)bv2natdiv 2− 1), 0)...) concat(1, 2) (1)bv2nat · 22 + (2)bv2nat extract(1) (1)bv2nat div 2 bvnot(1) 21 − (1)bv2nat + 1 bvand(1, 2) &((1)bv2nat, (2)bv2nat) ∃ ().(() ∧ (0 ≤ () < 2)) ∀ ().((0 ≤ () < 2) ⇒ ()) () (select () ()bv2nat) (store () ()bv2nat ()) (∀′.(0 ≤ ′ < 2) ⇒ ((select () ′) mod 2 = (select () ′) mod 2)) ⇒ () = () ⋀︀=1 Lem() ⊤ □ ∈ {∧, ∨, ¬, ⇒, ⇔}
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 framework2. 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 SMTInterpol3. 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.
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?
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 bit2https://ultimate.informatik.uni-freiburg.de and github.com/ultimate-pa/ultimate 3https://github.com/ultimate-pa/smtinterpol/tree/Intblasting
1010 1
10 100 CPU time of Eager [s] 100 1000 Memory used by Eager [MB] 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.
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.
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.
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 19 benchmarks where Lazy times out. Furthermore, on 426 benchmarks Lazy returns an error where 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.
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.
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. [4] Y. Zohar, A. Irfan, M. Mann, A. Niemetz, A. Nötzli, M. Preiner, A. Reynolds, C. Barrett, C. Tinelli, Bitprecise reasoning via int-blasting, in: B. Finkbeiner, T. Wies (Eds.), Verification, Model Checking, and Abstract Interpretation, Springer International Publishing, Cham, 2022, pp. 496–518. [5] F. Frohn, A calculus for modular loop acceleration, in: A. Biere, D. Parker (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I, volume 12078 of Lecture Notes in Computer Science, Springer, 2020, pp. 58–76. URL: https://doi.org/10.1007/978-3-030-45190-5_4. doi:10.1007/978-3-030-45190-5\_4. [6] P. Ganty, R. Iosif, F. Konecný, Underapproximation of procedure summaries for integer programs, Int. J. Softw. Tools Technol. Transf. 19 (2017) 565–584. URL: https://doi.org/10.1007/ s10009-016-0420-7. doi:10.1007/s10009-016-0420-7. [7] S. Gulwani, S. Srivastava, R. Venkatesan, Program analysis as constraint solving, in: R. Gupta, S. P. Amarasinghe (Eds.), Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, ACM, 2008, pp. 281–292.
URL: https://doi.org/10.1145/1375581.1375616. doi:10.1145/1375581.1375616. [8] M. Colón, S. Sankaranarayanan, H. Sipma, Linear invariant generation using non-linear constraint solving, in: W. A. H. Jr., F. Somenzi (Eds.), Computer Aided Verification, 15th International Conference, CAV 2003, Boulder, CO, USA, July 8-12, 2003, Proceedings, volume 2725 of Lecture Notes in Computer Science, Springer, 2003, pp. 420–432. URL: https://doi.org/10.1007/978-3-540-45069-6_ 39. doi:10.1007/978-3-540-45069-6\_39. [9] M. Colón, H. Sipma, Synthesis of linear ranking functions, in: T. Margaria, W. Yi (Eds.), Tools and Algorithms for the Construction and Analysis of Systems, 7th International Conference, TACAS 2001 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2001 Genova, Italy, April 2-6, 2001, Proceedings, volume 2031 of Lecture Notes in Computer Science, Springer, 2001, pp. 67–81. URL: https://doi.org/10.1007/3-540-45319-9_6. doi:10.1007/ 3-540-45319-9\_6. [10] A. R. Bradley, Z. Manna, H. B. Sipma, Linear ranking with reachability, in: K. Etessami, S. K.
Rajamani (Eds.), Computer Aided Verification, 17th International Conference, CAV 2005, Edinburgh, Scotland, UK, July 6-10, 2005, Proceedings, volume 3576 of Lecture Notes in Computer Science, Springer, 2005, pp. 491–504. URL: https://doi.org/10.1007/11513988_48. doi:10.1007/11513988\ _48. [11] A. Rybalchenko, Constraint solving for program verification: Theory and practice by example, in: T. Touili, B. Cook, P. B. Jackson (Eds.), Computer Aided Verification, 22nd International Conference, CAV 2010, Edinburgh, UK, July 15-19, 2010. Proceedings, volume 6174 of Lecture Notes in Computer Science, Springer, 2010, pp. 57–71. URL: https://doi.org/10.1007/978-3-642-14295-6_7. doi:10.1007/978-3-642-14295-6\_7. [12] M. Barth, M. Heizmann, Ultimate IntBlastingWrapper (2023). Available at https://smt-comp.github.
io/2023/system-descriptions/UltimateIntBlastingWrapper%2BSMTInterpol.pdf. [13] J. Christ, J. Hoenicke, A. Nutz, Smtinterpol: An interpolating SMT solver, in: A. F. Donaldson, D. Parker (Eds.), Model Checking Software - 19th International Workshop, SPIN 2012, Oxford, UK, July 23-24, 2012. Proceedings, volume 7385 of Lecture Notes in Computer Science, Springer, 2012, pp. 248–254. URL: https://doi.org/10.1007/978-3-642-31759-0_19. doi:10.1007/ 978-3-642-31759-0\_19. [14] Y. C. Liu, C. Pang, D. Dietsch, E. Koskinen, T. Le, G. Portokalidis, J. Xu, Source-level bitwise branching for temporal verification of lifted binaries, CoRR abs/2105.05159 (2021). URL: https: //arxiv.org/abs/2105.05159. arXiv:2105.05159. [15] A. Gurfinkel, A. Belov, J. Marques-Silva, Synthesizing safe bit-precise invariants, in: E. Ábrahám, K. Havelund (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 20th International Conference, TACAS 2014, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2014, Grenoble, France, April 5-13, 2014. Proceedings, volume 8413 of Lecture Notes in Computer Science, Springer, 2014, pp. 93–108. URL: https://doi.org/10.1007/ 978-3-642-54862-8_7. doi:10.1007/978-3-642-54862-8\_7. [16] A. Griggio, Efective word-level interpolation for software verification, in: P. Bjesse, A. Slobodová (Eds.), International Conference on Formal Methods in Computer-Aided Design, FMCAD ’11, Austin, TX, USA, October 30 - November 02, 2011, FMCAD Inc., 2011, pp. 28–36. URL: http: //dl.acm.org/citation.cfm?id=2157662. [17] T. Okudono, A. King, Mind the gap: Bit-vector interpolation recast over linear integer arithmetic, in: A. Biere, D. Parker (Eds.), Tools and Algorithms for the Construction and Analysis of Systems 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part I, volume 12078 of Lecture Notes in Computer Science, Springer, 2020, pp. 79–96. URL: https: //doi.org/10.1007/978-3-030-45190-5_5. doi:10.1007/978-3-030-45190-5\_5. [18] P. Backeman, P. Rümmer, A. Zeljic, Bit-vector interpolation and quantifier elimination by lazy reduction, in: N. S. Bjørner, A. Gurfinkel (Eds.), 2018 Formal Methods in Computer Aided Design, FMCAD 2018, Austin, TX, USA, October 30 - November 2, 2018, IEEE, 2018, pp. 1–10. URL: https://doi.org/10.23919/FMCAD.2018.8603023. doi:10.23919/FMCAD.2018.8603023. [19] A. Niemetz, M. Preiner, A. Reynolds, Y. Zohar, C. W. Barrett, C. Tinelli, Towards bit-widthindependent proofs in SMT solvers, in: P. Fontaine (Ed.), Automated Deduction - CADE 27 - 27th International Conference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, volume 11716 of Lecture Notes in Computer Science, Springer, 2019, pp. 366–384. URL: https://doi.org/10.1007/978-3-030-29436-6_22. doi:10.1007/978-3-030-29436-6\_22. [20] D. Beyer, P. Chien, N. Lee, Bridging hardware and software analysis with btor2c: A wordlevel-circuit-to-c translator, in: S. Sankaranarayanan, N. Sharygina (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Paris, France, April 22-27, 2023, Proceedings, Part II, volume 13994 of Lecture Notes in Computer Science, Springer, 2023, pp. 152–172. URL: https://doi.org/10.1007/978-3-031-30820-8_12. doi:10.1007/978-3-031-30820-8\_12. [21] H. Barbosa, C. W. Barrett, M. Brain, G. Kremer, H. Lachnitt, M. Mann, A. Mohamed, M. Mohamed, A. Niemetz, A. Nötzli, A. Ozdemir, M. Preiner, A. Reynolds, Y. Sheng, C. Tinelli, Y. Zohar, cvc5: A versatile and industrial-strength SMT solver, in: D. Fisman, G. Rosu (Eds.), Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part I, volume 13243 of Lecture Notes in Computer Science, Springer, 2022, pp. 415–442. URL: https://doi.org/10.1007/978-3-030-99524-9_24. doi:10.1007/978-3-030-99524-9\_24. [22] D. Beyer, S. Löwe, P. Wendler, Reliable benchmarking: Requirements and solutions, STTT 21 (2019) 1–29. doi:10.1007/s10009-017-0469-y.