QF_ABV doesn't allow keyword const

[LeventErkok]

For this benchmark:

(set-logic QF_ABV)
(define-fun s0 () (Array (_ BitVec 2) (_ BitVec 2)) ((as const (Array (_ BitVec 2) (_ BitVec 2))) #b00))
(check-sat)

z3 says:

(error "line 2 column 102: unknown constant const ((_ BitVec 2)) (Array (_ BitVec 2) (_ BitVec 2)) ")
sat

If you get rid of set-logic or use (set-logic ALL), the error isn't produced.

I think the const should be available as a constant regardless of the logic selection. (As a reference, cvc5 doesn't issue any complaints.)

[NikolajBjorner]

fixed