Error with Array sort as input to function

[SeanHeelan]

Hi,

When trying to use an array as an input to a function I get the following

(set-logic QF_AUFBV)

(define-fun Store-2 
  ((m (Array (_ BitVec 32) (_ BitVec 8))) (a (_ BitVec 32)))
  (Array (_ BitVec 32) (_ BitVec 8))
  (store m a #x08))

(check-sat)
(get-model)

$ boolector no_overlap.smt2
boolector: no_overlap.smt2:4:8: expected '_' at 'Array'

I can't see anything in the SMT-LIB2 standard that would forbid this and CVC4 seems not to mind.

$ cvc4 no_overlap.smt2 
sat
(error "Cannot get model when produce-models options is off.")

Is this a design decision in boolector or am I doing something wrong?

Thanks,
Sean

[mpreiner]

Hi Sean,

There is nothing wrong with the input - it is valid SMT2. This is currently not supported by Boolector.

[SeanHeelan]

Hey,

Thanks for the clarification.