branches are not supported when constructing bitvectors

[QDelta]

The following code will fail:

#lang rosette/safe
(define-symbolic b boolean?)
(bv (if b 1 2) 32)

The error message:

[assert] bv: expected a real, non-infinite, non-NaN number
  value: (ite b 1 2)

The expected result:

(ite b (bv #x00000001 32) (bv #x00000002 32))

I noticed that bv only accepts concrete values (real?). Is there a solution or a workaround (like implementing a bv wrapper)? It may be difficult for me to just replace all integers with bitvectors.

[anishathalye]

You want integer->bitvector, which works on symbolic values.

(define-symbolic* b boolean?)
(integer->bitvector (if b 1 2) (bitvector 32))

[QDelta]

You want integer->bitvector, which works on symbolic values.

(define-symbolic* b boolean?)
(integer->bitvector (if b 1 2) (bitvector 32))

That's exactly what I want, thank you!