Работа с битвек в pySmt

Question

Я изучаю битвек с pysmt. Но я встречаю некоторую проблему.

У меня есть три битвека, размер которых равен 1, называемых a,b,c. И я хочу закодировать (a<b)&c

      a = Symbol("a",BVType(1)) 
b = Symbol("b",BVType(1))
c = Symbol("c",BVType(1))
f = BVAnd(BVUlt(a,b),c)

Это терпит неудачу. Потому что, когда я пытаюсь выполнить операцию с BVUlt(a,b), он возвращает BOOL, но не BV(1). Так что я не могу сделать BV и позже.

Есть ли какое-нибудь решение, например, преобразовать BOOL в BVType(1)?