bug with datatype declaration

[robdockins]

The following script elicits a confusing error from Z3 with at least versions 4.7.1, 4.8.4 and 4.8.6 (the ones I happened to test)

$ cat z3bug.smt2
(set-option :global-declarations true)

(push 1)
(declare-datatypes (T1) ((Struct1 (mk-struct1 (struct1-proj0 T1)))))
(declare-fun x () (Struct1 Bool))
(pop 1)

(define-fun y () (Struct1 Bool) (mk-struct1 true))

$ z3 z3bug.smt2
(error "line 8 column 30: invalid declaration, function 'mk-struct1' (with the given signature) already declared")

$ z3 --version
Z3 version 4.8.6 - 64 bit

I expect y to be defined as a value equal to (mk-struct1 true), but instead I get the above error. This appears to be an interaction between the global-declarations option and the pop. Weirdly, the declaration of x also seems necessary to trigger the behavior.