MBP reports error "could not evaluate Boolean in model"

[dong-yf]

I tried mbp command in an example gen35.smt2.zip , it reports "could not evaluate Boolean in model".

sat
(error "line 37 column 105819: could not evaluate Boolean in model")

I add (get-model) between (check-sat) and mbp，then it seems to output normally.

sat...

sat
(
  (define-fun input11 () (_ BitVec 1)
    #b0)
  (define-fun input5 () (_ BitVec 1)
    #b0)
  (define-fun input9 () (_ BitVec 1)
    #b0)
  (define-fun state90.next () (_ BitVec 1)
    #b1)
  (define-fun input2 () (_ BitVec 1)
    #b0)
  (define-fun state63_nn () (_ BitVec 1)
    #b1)
  (define-fun state90_nn () (_ BitVec 1)
    #b0)
  (define-fun state63.next () (_ BitVec 1)
    #b0)
  (define-fun state90 () (_ BitVec 1)
    #b1)
  (define-fun state20.next () (_ BitVec 256)
    #x0000000000000000000000000000000000000000000000000000000000000000)
  (define-fun _monitor_0.next () Bool
    true)
  (define-fun state61.next () (_ BitVec 1)
    #b0)
  (define-fun state22.next () (_ BitVec 512)
    #x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
  (define-fun input6 () (_ BitVec 1)
    #b1)
  (define-fun _monitor_0 () Bool
    true)
  (define-fun state61_nn () (_ BitVec 1)
    #b0)
  (define-fun state20_nn () (_ BitVec 256)
    #x0000000000000000000000000000000000000000000000000000000000000000)
  (define-fun state22_nn () (_ BitVec 512)
    #x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
  (define-fun state22 () (_ BitVec 512)
    #x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
  (define-fun _monitor_0_nn () Bool
    true)
  (define-fun state61 () (_ BitVec 1)
    #b0)
  (define-fun state63 () (_ BitVec 1)
    #b0)
  (define-fun state20 () (_ BitVec 256)
    #x0000000000000000000000000000000000000000000000000000000000000000)
  (define-fun input8 () (_ BitVec 2)
    #b11)
  (define-fun input3 () (_ BitVec 1)
    #b1)
  (define-fun input17 () (_ BitVec 1)
    #b0)
  (define-fun input18 () (_ BitVec 1)
    #b0)
  (define-fun input16 () (_ BitVec 1)
    #b0)
  (define-fun input14 () (_ BitVec 1)
    #b0)
  (define-fun input10 () (_ BitVec 1)
    #b0)
  (define-fun input15 () (_ BitVec 1)
    #b0)
  (define-fun input4 () (_ BitVec 1)
    #b0)
  (define-fun input13 () (_ BitVec 279)
    #b000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
)
(let ((a!1 (bvor (bvnot (bvor (bvnot input5) input6)) (bvnot input6) input2)))
  (and (= state20_nn
          #x0000000000000000000000000000000000000000000000000000000000000000)
       (= state61_nn #b0)
       _monitor_0_nn
       (= input8 #b11)
       (= state22_nn
          #x00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000)
       (not (= input9 #b1))
       (not (= input5 #b1))
       (not (= input2 #b1))
       (not (= input11 #b1))
       (not (= input8 #b01))
       (= input6 #b1)
       (= input3 #b1)
       (= ((_ extract 282 282) state22_nn) #b0)
       (= state63_nn (bvnot a!1))
       (= state90_nn #b0)
       (= input5 #b0)
       (not (= input17 #b1))))

I wonder why it happens and if adding `(get-model)` will affect results. Thank you @hgvk94