Solution unsoundness in presence of as-array and sat.euf=true

[gsps]

The following produces an invalid model when run with
z3 -smt2 sat.euf=true (but not with z3 -smt2 tactic.default_tactic=smt sat.euf=true).
Applies to both version 4.8.12 and master (34f878f).

(declare-fun f (Int) Int)
(declare-const x Int)
(declare-const ff (Array Int Int))

; NB: Swapping the order of these two assertions leads to the expected unsat result!
(assert (= ff (_ as-array (f (Int) Int))))
(assert (= ff ((as const (Array Int Int)) 0)))

(assert (not (= (select ff x) 0)))
(check-sat)
(get-model)

[NikolajBjorner]

thanks for trying it out