yinyang icon indicating copy to clipboard operation
yinyang copied to clipboard

Parser rejects variables with prefix "bv"

Open wintered opened this issue 4 years ago • 0 comments

Commit: d8174eb

The parser currently rejects formulas such as the one below.

(declare-fun bv () (_ BitVec 10))                                               
(declare-fun a () Bool)                                                         
(assert (not (and (= ((_ extract 5 3) (_ bv96 8)) ((_ extract 4 2) (concat (_ bv121 7) 
((_ extract 0 0) bv)))) (= (concat (_ bv1 1) (ite a (_ bv0 1) (_ bv1 1))) ((_ extract 1 0) 
(ite a (_ bv6 3) (_ bv3 3)))))))
(check-sat)

Reason being the declared variable "bv" which seems to conflict with rules for bitvector constants such as "(_ bv0 1)". When there are no variables with prefix "bv", then parsing succeeds.

wintered avatar May 17 '21 11:05 wintered