Assertion violation at ctx_solver_simplify_tactic.cpp:131 (smt.threads 6)

[rainoftime]

Hi, for the following formula,

(set-logic QF_AUFNIA)
(set-option :smt.threads 6)
(declare-const v0 Bool)
(declare-const v10 Bool)
(declare-const v18 Bool)
(declare-const arr (Array Bool Bool))
(assert (distinct (store (store arr v10 false) v18 v0) arr (store arr v10 false)))
(check-sat-using ctx-solver-simplify)

z3 (commit 38e0968) throws an assertion violation

ASSERTION VIOLATION
File: ../src/smt/tactic/ctx_solver_simplify_tactic.cpp
Line: 131
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[NikolajBjorner]

I have to close this for now: the example illustrated a case where the context simplifier could be tuned. Furthermore, it stopped reproducing with and without the tuning.