ASSERTION VIOLATION File: ../src/qe/qsat.cpp Line: 884

[wintered]

Hi,
on the following formula z3 throws an assertion violation

(declare-datatypes () ((Lst nil (cons (hd Int) (tl Lst)))))
(declare-const l Lst)
(assert (exists ((x Int)) (= l (cons x nil))))
(apply qe2)

ASSERTION VIOLATION
File: ../src/qe/qsat.cpp
Line: 884
validate_assumptions(mdl, core)
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Revision: 8850000