Skip to content

Parser rejects variables with prefix "bv" #25

@wintered

Description

@wintered

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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    bugSomething isn't workingminor

    Type

    No type

    Projects

    No projects

    Milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions