Solving Quantified Bit-Vectors Using Invertibility Conditions

The majority of solvers that support quantified bit-vector logics employ instantiation-based techniques [8, 21, 22, 25], which aim to find conflicting ground instances of quantified formulas. For that, it is crucial to select good instantiations for the universal variables, or else the solver may be overwhelmed by the number of ground instances generated. For example, consider a quantified formula \(\psi = \forall x.\,(x + {s} \not \approx t) \) where x, s and t denote bit-vectors of size 32. To prove that \(\psi \) is unsatisfiable we can instantiate x with all \(2^{32}\) possible bit-vector values. However, ideally, we would like to find a proof that requires much fewer instantiations. In this example, if we instantiate x with the symbolic term \(t - s\) (the inverse of \(x + s \approx t \) when solved for x), we can immediately conclude that \(\psi \) is unsatisfiable since \((t - s) + {s} \not \approx t \) simplifies to false.

Operators in the theory of bit-vectors are not always invertible. However, we observe it is possible to identify quantifier-free conditions that precisely characterize when they are. We do that for a representative set of operators in the standard theory of bit-vectors supported by SMT solvers. For example, we have proven that the constraint \(x \cdot s \approx t\) is solvable for x if and only if \( (- s \mid s) \mathrel { \& } t \approx t\) is satisfiable. Using this observation, we develop a novel approach for solving quantified bit-vector formulas that utilizes invertibility conditions to generate symbolic instantiations. We show that invertibility conditions can be embedded into quantifier instantiations using Hilbert choice functions in a sound manner. This approach has compelling advantages with respect to previous approaches, which we demonstrate in our experiments.

Related Work. Quantified bit-vector logics are currently supported by the SMT solvers Boolector  [16], CVC4  [2], Yices  [7], and Z3  [6] and a Binary Decision Diagram (BDD)-based tool called Q3B  [14]. Out of these, only CVC4 and Z3 provide support for combining quantified bit-vectors with other theories, e.g., the theories of arrays or real arithmetic. Arbitrarily nested quantifiers are handled by all but Yices, which only supports bit-vector formulas of the form \(\exists \varvec{x} \forall \varvec{y}.\,Q[\varvec{x}, \varvec{y} ] \) [8]. For quantified bit-vectors, CVC4 employs counterexample-guided quantifier instantiation (CEGQI) [22], where concrete models of a set of ground instances and the negation of the input formula (the counterexamples) serve as instantiations for the universal variables. In Z3, model-based quantifier instantiation (MBQI) [10] is combined with a template-based model finding procedure [25]. In contrast to CVC4, Z3 not only relies on concrete counterexamples as candidates for quantifier instantiation but generalizes these counterexamples to generate symbolic instantiations by selecting ground terms with the same model value. Boolector employs a syntax-guided synthesis approach to synthesize interpretations for Skolem functions based on a set of ground instances of the formula, and uses a counterexample refinement loop similar to MBQI [21]. Other counterexample-guided approaches for quantified formulas in SMT solvers have been considered by Bjørner and Janota [4] and by Reynolds et al. [23], but they have mostly targeted quantified linear arithmetic and do not specifically address bit-vectors. Quantifier elimination for a fragment of bit-vectors that covers modular linear arithmetic has been recently addressed by John and Chakraborty [13], although we do not explore that direction in this paper.

We assume the usual notions and terminology of many-sorted first-order logic with equality (denoted by \(\approx \)). Let \(S\) be a set of sort symbols, and for every sort \({\sigma \in S}\) let \(X _{\sigma }\) be an infinite set of variables of sort \(\sigma \). We assume that sets \(X _{\sigma }\) are pairwise disjoint and define \(X\) as the union of sets \(X _{\sigma }\). Let \(\varSigma \) be a signature consisting of a set \(\varSigma ^s \!\subseteq S \) of sort symbols and a set \(\varSigma ^f \) of interpreted (and sorted) function symbols \(f^{\sigma _1 \cdots \sigma _n \sigma }\) with arity \(n \ge 0\) and \(\sigma _1, ..., \sigma _n, \sigma \in \varSigma ^s \). We assume that a signature \(\varSigma \) includes a Boolean sort \(\mathsf {Bool}\) and the Boolean constants \(\top \) (true) and \(\bot \) (false). Let \({\mathcal {I}}\) be a \(\varSigma \) -interpretation that maps: each \(\sigma \in \varSigma ^s \) to a non-empty set \(\sigma ^{\mathcal {I}} \) (the domain of \({\mathcal {I}}\)), with \(\mathsf {Bool} ^{\mathcal {I}} = \{ \top , \bot \}\); each \(x \in X _{\sigma } \) to an element \({x^{\mathcal {I}} \in \sigma ^{\mathcal {I}} }\); and each \(f^{\sigma _1 \cdots \sigma _n \sigma } \in \varSigma ^f \) to a total function \(f^{\mathcal {I}} \!\!: \sigma _1^{\mathcal {I}} \times ... \times \sigma _n^{\mathcal {I}} \rightarrow \sigma ^{\mathcal {I}} \) if \(n > 0\), and to an element in \(\sigma ^{\mathcal {I}} \) if \(n = 0\). If \(x \in X_\sigma \) and \(v \in \sigma ^{\mathcal {I}} \), we denote by \({\mathcal {I}} [x \mapsto v]\) the interpretation that maps x to v and is otherwise identical to \({\mathcal {I}} \). We use the usual inductive definition of a satisfiability relation \(\models \) between \(\varSigma \)-interpretations and \(\varSigma \)-formulas.

We assume the usual definition of well-sorted terms, literals, and formulas as \(\mathsf {Bool}\) terms with variables in \(X\) and symbols in \(\varSigma \), and refer to them as \(\varSigma \)-terms, \(\varSigma \)-atoms, and so on. A ground term/formula is a \(\varSigma \)-term/formula without variables. We define \(\varvec{x} = (x_1, ..., x_n)\) as a tuple of variables and write \(Q\varvec{x} \varphi \) with \(Q \in \{ \forall , \exists \}\) for a quantified formula \(Qx_1 \cdots Qx_n \varphi \). We use \(\mathrm {Lit}(\varphi )\) to denote the set of \(\varSigma \)-literals of \(\varSigma \)-formula \(\varphi \). For a \(\varSigma \)-term or \(\varSigma \)-formula e, we denote the free variables of e (defined as usual) as \({FV}(e)\) and use \(e[\varvec{x} ]\) to denote that the variables in \(\varvec{x}\) occur free in e. For a tuple of \(\varSigma \)-terms \(\varvec{t} = (t_1, ..., t_n)\), we write \(e[\varvec{t} ]\) for the term or formula obtained from e by simultaneously replacing each occurrence of \(x_i\) in e by \(t_i\). Given a \(\varSigma \)-formula \(\varphi [x]\) with \({x \in X _{\sigma }}\), we use Hilbert’s choice operator \(\varepsilon \)  [12] to describe properties of x. We define a choice function \(\varepsilon x.\,\varphi [x]\) as a term where x is bound by \(\varepsilon \). In every interpretation \({\mathcal {I}} \), \(\varepsilon x.\,\varphi [x]\) denotes some value \(v \in \sigma ^{\mathcal {I}} \) such that \({\mathcal {I}} [x \mapsto v]\) satisfies \(\varphi [x]\) if such values exist, and denotes an arbitrary element of \(\sigma ^{\mathcal {I}} \) otherwise. This means that the formula \(\exists x.\,\varphi [x] \Leftrightarrow \varphi [\varepsilon x.\,\varphi [x] ]\) is satisfied by every interpretation.

A theory T is a pair \((\varSigma , {I})\), where \(\varSigma \) is a signature and \({I}\) is a non-empty class of \(\varSigma \)-interpretations (the models of T) that is closed under variable reassignment, i.e., every \(\varSigma \)-interpretation that only differs from an \({{\mathcal {I}} \in {I}}\) in how it interprets variables is also in \({I}\). A \(\varSigma \)-formula \(\varphi \) is T-satisfiable (resp. T-unsatisfiable) if it is satisfied by some (resp. no) interpretation in \({I}\); it is T-valid if it is satisfied by all interpretations in \({I}\). A choice function \(\varepsilon x.\,\varphi [x]\) is (T-)valid if \(\exists x.\,\varphi [x]\) is (T-)valid. We refer to a term t as \(\varepsilon \) -(T-)valid if all occurrences of choice functions in t are (T-)valid. We will sometimes omit T when the theory is understood from context.

We will focus on the theory \(T_{BV} = (\varSigma _{BV}, {I} _{BV})\) of fixed-size bit-vectors as defined by the SMT-LIB 2 standard [3]. The signature \(\varSigma _{BV} \) includes a unique sort for each positive bit-vector width n, denoted here as \(\sigma _{[n]} \). Similarly, \(X _{[n]}\) is the set of bit-vector variables of sort \(\sigma _{[n]} \), and \(X _{BV} \) is the union of all sets \(X _{[n]}\). We assume that \(\varSigma _{BV}\) includes all bit-vector constants of sort \(\sigma _{[n]} \) for each n, represented as bit-strings. However, to simplify the notation we will sometimes denote them by the corresponding natural number in \(\{0, \ldots , 2^{n-1}\}\). All interpretations \({\mathcal {I}} \in {I} _{BV}\) are identical except for the value they assign to variables. They interpret sort and function symbols as specified in SMT-LIB 2. All function symbols in \(\varSigma ^f _{BV}\) are overloaded for every \(\sigma _{[n]} \! \in \varSigma ^s _{BV}\). We denote a \(\varSigma _{BV}\)-term (or bit-vector term) t of width n as \(t_{[n]}\) when we want to specify its bit-width explicitly. We use \(\text {max}_{s{[n]}}\) or \(\text {min}_{s{[n]}}\) for the maximum or minimum signed value of width n, e.g., \(\text {max}_{s{[4]}} = 0111\) and \(\text {min}_{s{[4]}}=1000\). The width of a bit-vector sort or term is given by the function \(\kappa \), e.g., \(\kappa (\sigma _{[n]}) = n\) and \(\kappa (t_{[n]}) = n\).

Without loss of generality, we consider a restricted set of bit-vector function symbols (or bit-vector operators) \(\varSigma ^f _{BV}\) as listed in Table 1. The selection of operators in this set is arbitrary but complete in the sense that it suffices to express all bit-vector operators defined in SMT-LIB 2.

This section formally introduces the concept of an invertibility condition and shows that such conditions can be used to construct symbolic solutions for a class of quantifier-free bit-vector constraints that have a linear shape.

Consider a bit-vector literal \(x + s \approx t\) and assume that we want to solve for x. If the literal is linear in x, that is, has only one occurrence of x, a general solution for x is given by the inverse of bit-vector addition over equality: \(x = t - s \). Computing the inverse of a bit-vector operation, however, is not always possible. For example, for \(x \cdot s \approx t\), an inverse always exists only if s always evaluates to an odd bit-vector. Otherwise, there are values for s and t where no such inverse exists, e.g., \(x \cdot 2 \approx 3\). However, even if there is no unconditional inverse for the general case, we can identify the condition under which a bit-vector operation is invertible. For the bit-vector multiplication constraint \(x \cdot s \approx t\) with \(x \notin {FV}(s) \cup {FV}(t) \), the invertibility condition for x can be expressed by the formula \( (- s \mid s) \mathrel { \& } t \approx t\).

An invertibility condition for a literal \(\ell [x]\) provides the exact conditions under which \(\ell [x]\) is solvable for x. We call it an “invertibility” condition because we can use Hilbert choice functions to express all such conditional solutions with a single symbolic term, that is, a term whose possible values are exactly the solutions for x in \(\ell [x]\). Recall that a choice function \(\varepsilon y.\,\varphi [y]\) represents a solution for a formula \(\varphi [x]\) if there exists one, and represents an arbitrary value otherwise. We may use a choice function to describe inverse solutions for a literal \(\ell [x]\) with invertibility condition \(\phi _\mathrm {c}\) as \(\varepsilon y.\,(\phi _\mathrm {c}\Rightarrow \ell [y])\). For example, for the general case of bit-vector multiplication over equality the choice function is defined as \( \varepsilon y.\,((- s \mid s) \mathrel { \& } t \approx t \;\Rightarrow \; y \cdot s \approx t)\).

Intuitively, the lemma states that when \(\ell [x]\) is satisfiable (under condition \(\phi _\mathrm {c}\)), any value returned by the choice function \(\varepsilon y.\,(\phi _\mathrm {c}\Rightarrow \ell [y]) \) is a solution of \(\ell [x]\) (and thus \(\exists x.\,\ell [x] \) holds). Conversely, if there exists a value v for x that makes \(\ell [x]\) true, then there is a model of \(T_{BV}\) that interprets \(\varepsilon y.\,(\phi _\mathrm {c}\Rightarrow \ell [y]) \) as v.

Now, suppose that \(\varSigma _{BV}\)-literal \(\ell \) is again linear in x but that x occurs arbitrarily deep in \(\ell \). Consider, for example, a literal \(s_1 \cdot (s_2 + x ) \approx t \) where x does not occur in \(s_1\), \(s_2\) or t. We can solve this literal for x by recursively computing the (possibly conditional) inverses of all bit-vector operations that involve x. That is, first we solve \(s_1 \cdot x' \approx t \) for \(x'\), where \(x'\) is a fresh variable abstracting \(s_2 + x \), which yields the choice function \( x' = \varepsilon y.\,((- s_1 \mid s_1) \mathrel { \& } t \approx t \Rightarrow s_1 \cdot y \approx t) \). Then, we solve \(s_2 + x \approx x'\) for x, which yields the solution \( x = x' - s_2 = \varepsilon y.\,((- s_1 \mid s_1) \mathrel { \& } t \approx t \Rightarrow s_1 \cdot y \approx t) - s_2 \).

Figure 1 describes in pseudo code the procedure to solve for x in an arbitrary literal \(\ell [x] = e[x] \bowtie t\) that is linear in x. We assume that e[x] is built over the set of bit-vector operators listed in Table 1. Function \(\mathsf {solve}\) recursively constructs a symbolic solution by computing (conditional) inverses as follows. Let function \(\mathsf {getInverse} (x, \ell [x])\) return a term \(t'\) that is the inverse of x in \(\ell [x]\), i.e., such that \(\ell [x] \Leftrightarrow x \approx t' \). Furthermore, let function \(\mathsf {getIC} (x, \ell [x])\) return the invertibility condition \(\phi _\mathrm {c}\) for x in \(\ell [x]\). If e[x] has the form \(\diamond (e_1, \ldots , e_n)\) with \(n > 0\), x must occur in exactly one of the subterms \(e_1, \ldots , e_n\) given that e is linear in x. Let d be the term obtained from e by replacing \(e_i\) (the subterm containing x) with a fresh variable \(x'\). We solve for subterm \(e_i[x]\) (treating it as a variable \(x'\)) and compute an inverse \(\mathsf {getInverse} (x', d[x'] \approx t)\), if it exists. Note that for a disequality \(e[x] \not \approx t\), it suffices to compute the inverse over equality and propagate the disequality down. (For example, for \(e_i[x] + s \not \approx t\), we compute the inverse \(t' = \mathsf {getInverse} (x', x'+ s \approx t) = t - s\) and recurse on \(e_i[x] \not \approx t' \).) If no inverse for \(e[x] \bowtie t\) exists, we first determine the invertibility condition \(\phi _\mathrm {c}\) for \(d[x']\) via \(\mathsf {getIC} (x', d[x'] \bowtie t)\), construct the choice function \(\varepsilon y.\,(\phi _\mathrm {c}\Rightarrow d[y] \bowtie t)\), and set it equal to \(e_i[x]\), before recursively solving for x. If \(e[x] = x\) and the given literal is an equality, we have reached the base case and return t as the solution for x. Note that in Fig. 1, for simplicity we omitted one case for which an inverse can be determined, namely \(x \cdot c \approx t\) where c is an odd constant.

Tables 2 and 3 list the invertibility conditions for bit-vector operators \(\{\cdot \), \(\bmod \), \(\div \), \( \mathrel { \& }\), \(\mid \), \(\mathop {>>}\), \(\mathop {>>_a}\), \(\mathop {<<}\), \(\circ \}\) over relations \(\{\) \(\approx \), \(\not \approx \), \(<_u\), \(>_u \}\). Due to space restrictions we omit the conditions for signed inequalities since they can be expressed in terms of unsigned inequality. We omit the invertibility conditions over \(\{\le _u \), \(\ge _u \}\) since they can generally be constructed by combining the corresponding conditions for equality and inequality—although there might be more succinct equivalent conditions. Finally, we omit the invertibility conditions for operators \(\{{\sim }\, \), \(-\), \(+ \}\) and literals \(x \bowtie t\) over inequality since they are basic bounds checks, e.g., for \(x <_s t\) we have \(t \not \approx \min \). The invertibility condition for \(x \not \approx t\) and for the extract operator is \(\top \).²

The idea of computing the inverse of bit-vector operators has been used successfully in a recent local search approach for solving quantifier-free bit-vector constraints by Niemetz et al. [17]. There, target values are propagated via inverse value computation. In contrast, our approach does not determine single inverse values based on concrete assignments but aims at finding symbolic solutions through the generation of conditional inverses. In an extended version of that work [18], the same authors present rules for inverse value computation over equality but they provide no proof of correctness for them. We define invertibility conditions not only over equality but also disequality and (un)signed inequality, and verify their correctness up to a certain bit-width.

In this section, we leverage techniques from the previous section for constructing symbolic solutions to bit-vector constraints to define a novel instantiation-based technique for quantified bit-vector formulas. We first briefly present the overall theory-independent procedure we use for quantifier instantiation and then show how it can be specialized to quantified bit-vectors using invertibility conditions.

We use a counterexample-guided approach for quantifier instantiation, as given by procedure \(\mathsf {CEGQI}_{\mathcal {S}}\) in Fig. 2. To simplify the exposition here, we focus on input problems expressed as a single formula in prenex normal form and with up to one quantifier alternation. We stress, though, that the approach applies in general to arbitrary sets of quantified formulas in some \(\Sigma \)-theory T with a decidable quantifier-free fragment. The procedure checks via instantiation the T-satisfiability of a quantified input formula \(\varphi \) of the form \(\exists \varvec{y} \forall \varvec{x}.\,\psi [\varvec{x},\varvec{y} ] \) where \(\psi \) is quantifier-free and \(\varvec{x} \) and \(\varvec{y} \) are possibly empty sequences of variables. It maintains an evolving set \(\varGamma \), initially empty, of quantifier-free instances of the input formula. During each iteration of the procedure’s loop, there are three possible cases: (1) if \(\varGamma \) is T-unsatisfiable, the input formula \(\varphi \) is also T-unsatisfiable and “unsat” is returned; (2) if \(\varGamma \) is T-satisfiable but not together with \(\lnot \psi [\varvec{y}, \varvec{x} ]\), the negated body of \(\varphi \), then \(\varGamma \) entails \(\varphi \) in T, hence \(\varphi \) is T-satisfiable and “sat” is returned. (3) If neither of previous cases holds, the procedure adds to \(\varGamma \) an instance of \(\psi \) obtained by replacing the variables \(\varvec{x}\) with some terms \(\varvec{t}\), and continues. The procedure \(\mathsf {CEGQI}_{}\) is parametrized by a selection function \(\mathcal {S}\) that generates the terms \(\varvec{t}\).

Procedure \(\mathsf {CEGQI}_{\mathcal {S}}\) is refutation-sound and model-sound for any selection function \(\mathcal {S}\), and terminating for selection functions that are finite and monotonic.

Thanks to this theorem, to define a T-satisfiability procedure for quantified \(\Sigma \)-formulas, it suffices to define a selection function satisfying the criteria of Definition 4. We do that in the following section for \(T_{BV}\).

We implemented our techniques in the solver \(\mathbf {cegqi}\) and considered four configurations \(\mathbf{{cegqi}}_{c}\), where c is one of {\(\mathbf {m}\), \(\mathbf {k}\), \(\mathbf {s}\), \(\mathbf {b}\)}, corresponding to the four selection function configurations described in Sect. 4. Out of these four configurations, \(\mathbf{{cegqi}}_{\mathbf {m}}\) is the only one that does not employ our new techniques but uses only model values for instantiation. It can thus be considered our base configuration. All configurations enable the optimizations described in Sect. 4.2 when applicable. We compared them against all entrants of the quantified bit-vector division of the 2017 SMT competition SMT-COMP: Boolector  [16], CVC4  [2], Q3B  [14] and Z3  [6]. With the exception of Q3B, all solvers are related to our approach since they are instantiation-based. However, none of these solvers utilizes invertibility conditions when constructing instantiations. We ran all experiments on the StarExec logic solving service [24] with a 300 s CPU and wall clock time limit and 100 GB memory limit.

We evaluated our approach on all 5,151 benchmarks from the quantified bit-vector logic (BV) of SMT-LIB [3]. The results are summarized in Table 4. Configuration \(\mathbf{{cegqi}}_{\mathbf {b}}\) solves the highest number of unsatisfiable benchmarks (4, 399), which is 30 more than the next best configuration \(\mathbf{{cegqi}}_{\mathbf {s}}\) and 37 more than the next best external solver, Z3. Compared to the instantiation-based solvers Boolector, CVC4 and Z3, the performance of \(\mathbf{{cegqi}}_{\mathbf {b}}\) is particularly strong on the h-uauto family, which are verification conditions from the Ultimate Automizer tool [11]. For satisfiable benchmarks, Boolector solves the most (581), which is 36 more than our best configuration \(\mathbf{{cegqi}}_{\mathbf {b}}\).

Overall, our best configuration \(\mathbf{{cegqi}}_{\mathbf {b}}\) solved 335 more benchmarks than our base configuration \(\mathbf{{cegqi}}_{\mathbf {m}}\). A more detailed runtime comparison between the two is provided by the scatter plot in Fig. 4. Moreover, \(\mathbf{{cegqi}}_{\mathbf {b}}\) solved 24 more benchmarks than the best external solver, Z3. In terms of uniquely solved instances, \(\mathbf{{cegqi}}_{\mathbf {b}}\) was able to solve 139 benchmarks that were not solved by Z3, whereas Z3 solved 115 benchmarks that \(\mathbf{{cegqi}}_{\mathbf {b}}\) did not. Overall, \(\mathbf{{cegqi}}_{\mathbf {b}}\) was able to solve 21 of the 79 benchmarks (26.6%) not solved by any of the other solvers. For 18 of these 21 benchmarks, it terminated after considering no more than 4 instantiations. These cases indicate that using symbolic terms for instantiation solves problems for which other techniques, such as those that enumerate instantiations based on model values, do not scale.

Interestingly, configuration \(\mathbf{{cegqi}}_{\mathbf {k}}\), despite having the strong guarantees given by Theorem 9, performed relatively poorly on this set (with 4, 571 solved instances overall). We attribute this to the fact that most of the quantified formulas in this set are not unit linear invertible. In total, we found that only 25.6% of the formulas considered during solving were unit linear invertible. However, only a handful of benchmarks were such that all quantified formulas in the problem were unit linear invertible. This might explain the superior performance of \(\mathbf{{cegqi}}_{\mathbf {s}}\) and \(\mathbf {\mathbf{{cegqi}}_{\mathbf {b}}}\) which use invertibility conditions but in a less monolithic way.  For some intuition on this, consider the problem \(\forall x.\,(x > a \vee x < b)\) where a and b are such that \(a>b\) is \(T_{BV}\)-valid. Intuitively, to show that this formula is unsatisfiable requires the solver to find an x between b and a. This is apparent when considering the dual problem \(\exists x.\,(x \le a \wedge x \ge b)\). Configuration \(\mathbf{{cegqi}}_{\mathbf {b}}\) is capable of finding such an x, for instance, by considering the instantiation \(x \mapsto a\) when solving for the boundary point of the first disjunct. Configuration \(\mathbf{{cegqi}}_{\mathbf {k}}\), on the other hand, would instead consider the instantiation of x for two terms that witness \(\varepsilon \)-expressions: some \(k_1\) that is never smaller than a, and some \(k_2\) that is never greater that b. Neither of these terms necessarily resides in between a and b since the solver may subsequently consider models where \(k_1 > b\) and \(k_2 < a\). This points to a potential use for invertibility conditions that solve multiple literals simultaneously, something we are currently investigating.

We have presented a new class of strategies for solving quantified bit-vector formulas based on invertibility conditions. We have derived invertibility conditions for the majority of operators in a standard theory of fixed-width bit-vectors. An implementation based on this approach solves over 25% of previously unsolved verification benchmarks from SMT LIB, and outperforms all other state-of-the-art bit-vector solvers overall.

In future work, we plan to develop a framework in which the correctness of invertibility conditions can be formally established independently of bit-width. We are working on deriving invertibility conditions that are optimal for linear constraints, in the sense of admitting the simplest propositional encoding. We also are investigating conditions that cover additional bit-vector operators, some cases of non-linear literals, as well as those that cover multiple constraints. While this is a challenging task, we believe efficient syntax-guided synthesis solvers can continue to help push progress in this direction. Finally, we plan to investigate the use of invertibility conditions for performing quantifier elimination on bit-vector constraints. This will require a procedure for deriving concrete witnesses from choice expressions.