Setting smt.mbqi.id causes result to switch from unsat to sat

[ole-thoeb]

While trying to implement limited functions we needed to disable MBQI.
Since the usual approach of disabling both smt.mbqi and auto_config caused flaky behaviour in some of our tests, we had the
(unconventional) idea of using smt.mbqi.id to achieve this goal.

The documentation states:

Only use model-based instantiation for quantifiers with id's beginning with string

So the idea is to set it to some value that is not a prefix of any quantifier id, but this had surprising behaviour.
Take this program

; uncommenting the next line makes the problem sat
; (set-option :smt.mbqi.id "abcdefghij")

(declare-datatypes (($Fuel 0)) ((($Z) ($S (f $Fuel)))))
(declare-sort $List 0)
(declare-fun exp ($Fuel Real Int) Real)
(declare-fun len ($List) Int)
(declare-fun pop ($List) $List)
(declare-fun l_0!17 () $List)
(declare-fun init_l!16 () $List)
(assert (forall ((base!9 Real) (exponent!10 Int) (fuel!8 $Fuel))
  (! (=> (and (>= base!9 0.0) (>= exponent!10 0))
         (>= (exp fuel!8 base!9 exponent!10) 0.0))
     :qid |exp(return_invariant)|)))
(assert (forall ((base!9 Real) (exponent!10 Int) (fuel!11 $Fuel))
  (! (let ((a!1 (* base!9
                   (exp fuel!11
                        base!9
                        (ite (>= exponent!10 1) (- exponent!10 1) 0)))))
       (=> (and (>= base!9 0.0) (>= exponent!10 0))
           (= (exp fuel!11 base!9 exponent!10)
              (ite (= exponent!10 0) (to_real 1) a!1))))
     :pattern ((exp ($S fuel!11) base!9 exponent!10))
     :qid |exp(definitional)|)))
(assert (forall ((base!9 Real) (exponent!10 Int) (fuel!12 $Fuel))
  (! (=> (and (>= base!9 0.0) (>= exponent!10 0))
         (= (exp ($S fuel!12) base!9 exponent!10)
            (exp fuel!12 base!9 exponent!10)))
     :pattern ((exp ($S fuel!12) base!9 exponent!10))
     :qid |exp(fuel_synonym)|)))
(assert (forall ((l!13 $List))
  (! (=> and (>= (len l!13) 0)) :qid |len(return_invariant)|)))
(assert (forall ((l!15 $List))
  (! (let ((a!1 (= (len (pop l!15)) (ite (>= (len l!15) 1) (- (len l!15) 1) 0))))
       (=> and a!1))
     :qid |len(pop)|)))
(assert (let ((a!1 (* (/ 1.0 2.0) (exp ($S $Z) (/ 1.0 2.0) (len (pop l_0!17)))))
      (a!2 (ite (<= 0.0 (exp ($S $Z) (/ 1.0 2.0) (len l_0!17)))
                0.0
                (exp ($S $Z) (/ 1.0 2.0) (len l_0!17))))
      (a!5 (* (/ 1.0 2.0) (ite (= (len init_l!16) 1) 1.0 0.0))))
(let ((a!3 (<= (exp ($S $Z) (/ 1.0 2.0) (len l_0!17))
               (ite (<= (len l_0!17) 0) 1.0 (+ a!1 (* (/ 1.0 2.0) a!2))))))
(let ((a!4 (or a!3
               (<= (exp ($S $Z) (/ 1.0 2.0) (len init_l!16)) (ite a!3 1.0 0.0)))))
(let ((a!6 (<= a!5
               (ite a!4
                    (exp ($S $Z) (/ 1.0 2.0) (len init_l!16))
                    (ite a!3 1.0 0.0)))))
  (not (or (and (not a!4) a!3) a!6)))))))

(check-sat)

uncommenting the set-option turns the result from unsat to sat (Tested with 4.13.3 - 64 bit and 4.13.4 - 64 bit) and the given model is

(
  ;; universe for $List:
  ;;   $List!val!1 $List!val!0
  ;; -----------
  ;; definitions for universe elements:
  (declare-fun $List!val!1 () $List)
  (declare-fun $List!val!0 () $List)
  ;; cardinality constraint:
  (forall ((x $List)) (or (= x $List!val!1) (= x $List!val!0)))
  ;; -----------
  (define-fun init_l!16 () $List
    $List!val!0)
  (define-fun l_0!17 () $List
    $List!val!1)
  (define-fun exp ((x!0 $Fuel) (x!1 Real) (x!2 Int)) Real
    0.0)
  (define-fun len ((x!0 $List)) Int
    (ite (= x!0 $List!val!1) 15922
      1))
  (define-fun pop ((x!0 $List)) $List
    $List!val!1)
)

The model seems wrong. In particular, setting exp to always be 0 is in conflict with exp(definitional).
Setting model_validate did not change anything.

Does anybody know what is happening here? Are we misinterpreting what the option does? Is our usage unsoud or is this a bug?
Any insight is appreciated!