search

uuverifiers / eldarica

The Eldarica model checker
Other
80 stars 23 forks source link

Eldarica rejects valid smt2 syntax for recognizers #49

Closed hgvk94 closed 1 year ago

hgvk94 commented 1 year ago 
(declare-datatypes ((MList 0)) (((mcons  (mhead Int) (mtail MList)) (mnill))))
(declare-fun x () MList)
(declare-fun y () MList)
(assert (and ((_ is mcons) x) (= (mtail x) y) (= y mnill))) ;;valid according to smtlib but Eldarica does not accept this
;; (assert (and (is-mcons x) (= (mtail x) y) (= y mnill))) ;;ALL smt solvers accept this recognizer
(check-sat)

Eldarica (version 2.0.8) does not like the first assertion but it is valid according to smtlib.

More context: I am trying to write a pretty printer for CHC benchmarks containing ADTs. I would like to use the first representation, but only if Eldarica supports it.

pruemmer commented 1 year ago

This is fixed on Master, and will be working in the next version 2.0.9!

hgvk94 commented 1 year ago

great. Thanks !!