Eldarica misses to emit a parser error

[kensingRichardt]

Hello everyone,

it seems that eldarica's parser misses to report an error for the following SMT-Code:

(declare-fun p ((Array Int Bool)) Bool)

(assert
  (p
    (store ((as const (Array Int Bool)) false) 1 3)
  )
)

The assertion is not well-sorted, i.e. we store in an array of type Bool an Int value. However eldarica outputs

$ ~/eldarica/eld -assert  test.smt2 
sat

[pruemmer]

Thank you for the report; I'm marking this issue as an improvement of the front-end, to be taken care of at some point. We are aware that there are some cases, including this one, in which the parser accepts ill-typed formulas, and Eldarica will happily solve them. This is a bug, but not a very serious one, since even the ill-typed formula makes perfect sense in the internal representation of Eldarica, where Bool is encoded as Int.