(proof, rewriter.pull_cheap_ite) Assertion violation at ../src/ast/rewriter/rewriter_def.h Line: 176

[muchang]

Hi,
For this formula:

(set-option :proof true)
(set-option :rewriter.pull_cheap_ite true)
(declare-datatypes ((a 0)) (((j) (b))))
(declare-sort c 0)
(declare-fun d () (Array c a))
(declare-fun f () (Array c a))
(declare-fun h () (Array c a))
(declare-fun k () (Array c (Array c a)))
(declare-fun l () (Array c (Array c a)))
(assert (forall ((e c)) (= (select k e) d)))
(assert (forall ((m c)) (= (select f m) j)))
(assert (forall ((g c)) (= (select l g) f)))
(assert (forall ((i c)) (= (select h i) b)))
(check-sat)

Z3 throws out an assertion violation:

ASSERTION VIOLATION
File: ../src/ast/rewriter/rewriter_def.h
Line: 176
rewrites_to(r, pr)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: 2695221