z3: как преобразовать логическую сортировку в сортировку по битовому вектору

Я делаю символическую интерпретацию инструкций x86. Например, для инструкции cmp знак сравнения и равенство операндов хранятся в двух битах регистра eflags.

Вот мой код:

/* s1,s2 are source operands of sort bit-vector
 *       of 32 bits (defined somewhere else)
 * ctx is the context (defined somewhere else)
 * eflags is of sort bit-vector of 32 bits (initialized somewhere else)
 */

#define ZF_INDEX 6

Z3_ast ZF,OF,CF;              /* eflags bits */
ZF = Z3_mk_eq(ctx,s1,s2);
Z3_ast zf_mask = Z3_mk_rotate_left(ctx, ZF_INDEX ,Z3_mk_zero_ext(ctx,31,ZF));
eflags = Z3_mk_bvand(ctx,eflags, zf_mask);

Проблема в том, что я не нашел никакой функции в z3 API для преобразования (предполагаемой) логической сортировки (ZF в моем примере) в битовый вектор (любой длины).

Я думал о создании функции с оператором ite в ZF, которая возвращала бы битовый вектор, но я хотел бы знать традиционный способ сделать это.

Спасибо,

Хейджи.