Wrong model printing for arrays

[Halbaroth]

Alt-Ergo (next - 963e40c) doesn't print correctly the model for the following input file:

(set-logic ALL)
(declare-const x Int)
(declare-const y Int)
(declare-const a1 (Array Int Int))
(declare-const a2 (Array Int Int))
(assert (= (select a1 x) x))
(assert (= (store a1 x y) a1))
(check-sat)
(get-model)

The actual model:

unknown

(model
  
 ; Functions

 ; Constants

(define-fun a1 () (Array Int Int) a1)

(define-fun x () Int 0)

(define-fun y () Int 0)

 ; Arrays not yet supported


)

unknown

[Gbury]

Rather, a model would be any assignment where:

• x = y
• a1 binds x to x

[hra687261]

The model is not wrong. It's printing is wrong. Since x = y = 0 and a1 binds x to y.
The printing should look something like what Z3 produces:

sat
(
  (define-fun a1 () (Array Int Int)
    (store ((as const (Array Int Int)) 2) 3 3))
  (define-fun x () Int
    3)
  (define-fun y () Int
    3)
  (define-fun a2 () (Array Int Int)
    ((as const (Array Int Int)) 0))
)
(
  (define-fun a1 () (Array Int Int)
    (store ((as const (Array Int Int)) 2) 3 3))
  (define-fun x () Int
    3)
  (define-fun y () Int
    3)
  (define-fun a2 () (Array Int Int)
    ((as const (Array Int Int)) 0))
)

A default value with const, plus a set of bindings with stores.
Can you fix the text of the issue?