I wrote a Yices SMT code with following expressions.
(define f1::(-> (bitvector 2) (bitvector 2)))
(define t::(bitvector 2))
(assert (= t 0b00))
(assert (= f1 (update f1 (t) 0b01)))
(assert (= f1 (update f1 (0b01) 0b11)))
(assert (bv-gt (f1 t) 0b00))
(check)
;(↑sat)
However, when I tried to convert above expression into C language code, I cannot find a method to expresses (f1 t). I would like to ask if there is any C API function to extract a value as term of my function.(assert (bv-gt (f1 t) 0b00))
I wrote a Yices SMT code with following expressions.
However, when I tried to convert above expression into C language code, I cannot find a method to expresses
(f1 t)
. I would like to ask if there is any C API function to extract a value as term of my function.(assert (bv-gt (f1 t) 0b00))