Soundness bug: satisfiable QF_S formula accepts model but is reported unsat

[wintered]

Hi,

on the following formula Z3 returns unsat on this satisfiable formula.

(declare-fun value2 () String)
(declare-fun key1 () String)
(declare-fun value1 () String)
(declare-fun key2 () String)                                  
                                                                                
(assert                                                                         
(and                                                                            
    (= (str.at (str.substr value1 0 1) 0) "\r")                                 
    (not                                                                        
        (= (str.at (str.substr value1 (+ (str.indexof value1 "=" 0) 1)          
        (- 1 (+ (str.indexof value1 "=" 0) 1))) 0) "\f")                        
    )                                                                           
    (= (ite (= (str.len (str.substr value1 0 (- (str.indexof value1 "=" 0) 0))) 0) 1 0) 0)) 
)                                                                               
(check-sat)                                                                     
(get-model)  

When feeding the following model to the formula, it is satisfiable

(define-fun value2 () String "")
(define-fun key1 () String "")
(define-fun value1 () String "\r=")
(define-fun key2 () String "")

OS: Ubuntu 18.04
Revision: 17d67c1