Crash on too long extraction

[Halbaroth]

Alt-Ergo crashes on the following input:

(set-logic BV)
(declare-const x (_ BitVec 11))
(assert (= x ((_ extract 10 0) #b1010)))
(check-sat)

Output:

Fatal error: exception Invalid_argument("String.sub / Bytes.sub")

Command line:

$ alt-ergo --frontend dolmen test.smt2

I think the issue comes from the new canonizer in bitv.ml

[bclement-ocp]

The issue does not come from the canonizer, it comes from the fact that the file is ill-typed. Such term should never reach the canonizer (#b1010 has type (_ BitVec 4) and (_ extract 10 0) can only be called on a bitvector term of size n > 10).

[Halbaroth]

Yes, you are right. According to the SMTLIB, the type of the extract primitive is :

All function symbols with declaration of the form

      ((_ extract i j) (_ BitVec m) (_ BitVec n))

    where
    - i, j, m, n are numerals
    - m > i ≥ j ≥ 0,
    - n = i - j + 1

Dolmen should reject this input file?

[bclement-ocp]

This is a dolmen bug and should be reported as such, but in the meantime we should catch this in d_cnf.

(Edit: and by "catch this" I mean that we should raise a typing error in that case)

[Halbaroth]

Ok, I will report the bug on Dolmen repo and propose a temporary fix since we won't wait a new release of Dolmen for the next release of AE.