Rodrigo Otoni

The initial idea is to have an alternative SMT encoding using arrays as an experimental feature, enabled under a CLI option. - [x] Write an ADR to describe the new...

Odd that this happens on `simulate` but not on `check`. At least here (on my local setup) the error happens consistently on the third symbolic run.

Seems to be an interesting idea. After having a quick look about it, I wonder if this would allow us to use specialized solvers, as described [here](https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-incrementality).

@konnov after #2549 is merged, only #1589 will remain open. Should we close this issue?

I'm not using any parameters when running Z3. I built from `master` to check and it gives me the model you posted, which is different from the one obtained with...

The model you posted is indeed valid, apologies for the mistake. The one I got with master is not identical to it actually. Model from `master` (62e1ec069853b22bb82090c17dfbcd013dfd5088) ``` (define-fun main_1...