[90] % ./z3debug model_validate=true small.smt2
sat
(error "line 4 column 10: an invalid model was generated")
(model 
  (define-fun a () String
    "\x00\x00\f")
)
[91] % cat small.smt2 
(declare-fun a () String)
(assert (= (str.at (str.substr (str.substr a 1 (- (str.len a) 1)) 1 
        (- (str.len (str.substr a 1 (- (str.len a) ))) 1)) 0) "\f"))
(check-sat)  
(get-model)      
[92] %