Performance impact of lambda array representation

[OrangeRoof]

The following SMTLIB2 snippet declares the same array and asks Z3 to repeat it in two ways - using store and lambda:

(declare-const x (Array Int Int))

(push)
(assert (= x (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store (store ((as const (Array Int Int)) 339) 7 332) 107 334) 328 340) 88 343) 0 98) 70 333) 13 330) 26 342) 35 331) 80 336) 27 338) 53 337) 329 341) 154 335) 127 245) 6 334)))
(check-sat) 
(pop)

(push)
(assert (= x (lambda ((b!0 Int)) (ite (= b!0 6) 334 (ite (= b!0 127) 345 (ite (= b!0 154) 335 (ite (= b!0 329) 341 (ite (= b!0 53) 337 (ite (= b!0 27) 338 (ite (= b!0 80) 336 (ite (= b!0 35) 331 (ite (= b!0 26) 342 (ite (= b!0 13) 330 (ite (= b!0 70) 333 (ite (= b!0 0) 98 (ite (= b!0 88) 343 (ite (= b!0 328) 340 (ite (= b!0 107) 344 (ite (= b!0 7) 332 339)))))))))))))))))))
(check-sat)
(pop)

On a few Linux machines, we quickly get sat in response to the first (check-sat), with no reply from the second (check-sat) for significantly longer until eventually returning unknown.
I know these two have different implementations within Z3 and may not perform equivalently.
However, my use case requires using the ALIA logic, which prevents using the as const representation. Adding (set-logic ALIA) to the beginning of the script yields an error parsing as const, and (get-model) indicates the assert failed. From past comments on issues, this seems to be intended behavior.

Is there any way of representing larger arrays under ALIA with reasonable performance? Thanks in advance.

[NikolajBjorner]

lambda isn't part of ALIA either, just happen to be allowed by z3.
for z3 ALIA a hint to tell which default parameters to use. It otherwise enforces the signature.
It is always possible to improve detection of the cases where lambdas can be handled in a complete way. Currently it just looks for extensional uses of lambda instantiates indices indiscriminately and then gives up if it cannot determine unsat.