(smt.random_seed=2, trace, smt.dack.eq) Assertion violation at ../src/ast/ast.h Line: 491 (debug) or ../src/ast/ast.cpp Line: 431 (release)

[muchang]

Hi,
For this case,
Z3 throws out an assertion violation:

[596] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.h
Line: 491
m_ref_count > 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[597] % z3release small.smt2
unknown
[598] % z3release small.smt2
unknown
[599] % z3release small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 431
UNREACHABLE CODE WAS REACHED.
Z3 4.8.8.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[600] % z3san small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 431
UNREACHABLE CODE WAS REACHED.
Z3 4.8.8.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[601] % z3san small.smt2
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 431
UNREACHABLE CODE WAS REACHED.
Z3 4.8.8.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
[602] % 
[602] % cat small.smt2
(set-option :smt.random_seed 2)
(set-option :trace true)
(set-option :smt.dack.eq true)
(declare-datatypes ((Lst 0) (Nat 0)) (((cons (a Nat) (tail Lst)) (nil)) ((succ (b Nat)) c)))
(declare-fun len (Lst) Nat)
(declare-fun append (Lst Lst) Lst)
(assert (forall ((x Lst)) (= (append nil x) x)))
(assert (forall ((x Nat) (d Lst) (z Lst)) (= (append (cons x d) z) (cons x (append d z)))))
(assert (not (forall ((x Lst) (d Lst)) (= (len (append x d)) (len (append d x))))))
(check-sat-using qfidl)
[603] %

The assertion violation is flaky for release build.

OS: Ubuntu 18.04
Commit: 9f6a733