z3Py: Cast BoolRef to one-bit BitVecRef
<p>Is it possible to cast <code>BoolRef</code> to a one-bit-long <code>BitVecRef</code> in z3Py? In my design, it is required that a <code>BitVecRef</code> is returned from a comparison between two other <code>BitVecRef</code>'s. This would be similar to casting a python <code>bool</code> to an <code>int</code>. Here is an example of its use:</p>

<pre><code>bv1, bv2, added = z3.BitVecs('bv1 bv2 added', 4)
res = z3.BitVec('res', 1)
s = z3.Solver()
s.add(res == (bv1 &lt; bv2))
s.add(added == added + z3.ZeroExt(3, res))
</code></pre>

<p>This would be ideal, but the type of <code>(bv1 &lt; bv2)</code> is <code>Boolref</code>, and it throws a "sort mismatch" error. Is there a way to cast the result of <code>(bv1 &lt; bv2)</code> so that <code>res</code> can asserted equal to it?</p>

<p>Bit-vectors can't be casted to Boolean automatically. The usual approach is to wrap them in if-then-elses, e.g., in this example, instead of </p>

<pre><code>s.add(res == (bv1 &lt; bv2))
</code></pre>

<p>we can say</p>

<pre><code>c = If(bv1 &lt; bv2, BitVecVal(1, 1), BitVecVal(0, 1))
s.add(res == c)
</code></pre>

python casting z3 z3py bitvector