Caveat: I don't know whether the following is intended behaviour or not.

With some satisfiable formulae containing quantifiers Z3 returns models where get-value for a Bool variable produces a quantified expression. The following is a reduced example:

(set-option :produce-models true)

(declare-fun |main::1::i!0@1#1| () (_ BitVec 32))
(declare-fun |main::1::2::1::j!0@1#1| () (_ BitVec 32))
(define-fun B4 () Bool (= (bvsrem |main::1::i!0@1#1| (_ bv2 32)) (_ bv0 32)))
(define-fun B5 () Bool (=> (and true B4) (not (let ((?sum (bvadd ((_ sign_extend 1) |main::1::2::1::j!0@1#1|) ((_ sign_extend 1) |main::1::2::1::j!0@1#1|)))) (not (= ((_ extract 32 32) ?sum) ((_ extract 31 31) ?sum)))))))
(declare-fun B6 () Bool)

(assert (= B6 (=> (and true B4) (exists ((|main::1::2::1::j!0@1#0| (_ BitVec 32))) (= |main::1::i!0@1#1| (bvadd |main::1::2::1::j!0@1#0| |main::1::2::1::j!0@1#0|))))))
(assert (or (not B5) (not B6)))

(check-sat)

(get-value (B4))
(get-value (B5))
(get-value (B6))
(get-value (|main::1::2::1::j!0@1#1|))
(get-value (|main::1::i!0@1#1|))

(exit)

Both Z3 4.8.12 and 4.13.4 produce exactly the same result as follows:

sat
((B4 true))
((B5 false))
((B6 (exists ((|main::1::2::1::j!0@1#0| (_ BitVec 32)))
  (= (bvmul #x00000002 |main::1::2::1::j!0@1#0|) #x00000000))))
((|main::1::2::1::j!0@1#1| #x40000000))
((|main::1::i!0@1#1| #x00000000))

1. Is this behaviour expected?
2. Is there a way to make Z3 evaluate the quantified expression before returning the model?
3. Some related information:

• Section 4.2.6 of the SMT-LIB standard (v2.7) says that get-value "returns for each $t_i$ a value term $v_i$" with the footnote "Recall that value terms are particular ground terms defined in a logic for each sort (see Subsection 5.5.1)." Is the above (exists ... ) considered a ground term?
• cvc5 (1.2.0) requires the use of --no-model-var-elim-uneval to avoid the same problem, though Use subsolver in get-value when necessary cvc5/cvc5#12002 should address this.
• Bitwuzla (0.7.0) readily returns true as value of B6.
• The above example is reduced from an example from CBMC's regression test suite, but CBMC users actually face this problem in real-world scenarios, see CBMC cannot understand Z3 generating a quantified expression in a counter-example diffblue/cbmc#8679.