fp.xform.quantify_arrays horn Assertion violation at ../src/muz/base/dl_rule_set.cpp Line: 369

[muchang]

Hi,
For this formula:

(set-option :fp.xform.quantify_arrays true)
(declare-fun b ((Array Int Int)) Bool)
(assert (forall ((a (Array Int Int))) (b a)))
(assert (forall ((a (Array Int Int))) (=> (b a) (b a))))
(assert (forall ((a (Array Int Int))) (not (b a))))
(check-sat-using horn)

Z3 throws out an assertion violation:

Failed to verify: close()
ASSERTION VIOLATION
File: ../src/muz/base/dl_rule_set.cpp
Line: 369
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: 5c9fd90