get-model returns not all variables

[pjljvandelaar]

Running z3 with the following model

(get-info :name)
(get-info :version)
(set-logic ALL)
(set-option :produce-models true)
(set-info :smt-lib-version 2.5)

(push)
(declare-fun s1() String)
(assert (str.in.re s1 (re.+ (re.range "a" "z"))))
(check-sat)
(get-model)
(pop)
(check-sat)
(get-model)

on windows 10
provides the expected output:

PS C:\experiments\z3> z3 .\nest.smt2
(:name "Z3")
(:version "4.8.5")
sat
(model
  (define-fun s1 () String
    "b")
)
sat
(model
)

However, when the nineth line is removed, I get a model I did not expect.
Thus z3 with this model

(get-info :name)
(get-info :version)
(set-logic ALL)
(set-option :produce-models true)
(set-info :smt-lib-version 2.5)

(push)
(declare-fun s1() String)
(check-sat)
(get-model)
(pop)
(check-sat)
(get-model)

produces

(:name "Z3")
(:version "4.8.5")
sat
(model
)
sat
(model
)

Why does the model not contain variable s1 with a value?

According to the standard on page 61,
(get-model) returns a list (d1 ··· dk) of definitions specifying **all** and only the current userdeclared function symbols {g1,...,gm} in the current model A

Note that get-value works as expected:

(get-info :name)
(get-info :version)
(set-logic ALL)
(set-option :produce-models true)
(set-info :smt-lib-version 2.5)

(push)
(declare-fun s1() String)
(check-sat)
(get-model)
(get-value (s1))
(pop)
(check-sat)
(get-model)

provides

(:name "Z3")
(:version "4.8.5")
sat
(model
)
((s1 ""))
sat
(model
)

Note that cvc4 does include s1 in its model:

PS C:\experiments\z3> cvc4 --incremental .\nest.smt2
(:name "cvc4")
(:version "1.7")
sat
(model
(define-fun s1 () String "")
)
sat
(model
)