(datatype) Assertion error at src/smt/mam.cpp:1664, src/util/map.h:150

[rainoftime]

Hi, for the following formula, z3 322531e

(declare-sort S$t$type)
(declare-sort resource$type)
(declare-datatypes ((BOOL 0)) (((Truth))))
(declare-sort process$type)
(declare-fun S$mem (process$type S$t$type) BOOL)
(declare-fun null () resource$type)
(declare-fun S$empty () S$t$type)
(assert (forall ((handles$1 (Array resource$type S$t$type))) (forall ((handles (Array resource$type S$t$type))) (and (forall ((e process$type)) (= Truth (S$mem e S$empty))) (exists ((p process$type) (r resource$type)) (not (let (($x242 (= Truth (S$mem p (handles$1 r)))))))) (forall ((p process$type) (r resource$type)) (let (($x231 (and (= r null) (= Truth (S$mem p (handles r))))))))))))
(check-sat)

ASSERTION VIOLATION
File: ../src/smt/mam.cpp
Line: 1664
curr != 0
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[rainoftime]

src/util/map.h:150

(declare-datatypes ((A_llist_a_llist_prod$ 0)))
(declare-fun swap$ (A_llist_a_llist_prod$) A_llist_a_llist_prod$)
(assert (forall ((?v0 A_llist_a_llist_prod$)) (= ?v0 (swap$ ?v0))))
(check-sat-using ctx-solver-simplify)

(error "line 1 column 47: invalid datatype declaration, '(' expected got A_llist_a_llist_prod$")
ASSERTION VIOLATION
File: ../src/util/map.h
Line: 150
e
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

release mode segfault