(declare-fun a () Int)
(declare-fun d () Int) 
(declare-fun k () Int)
(declare-fun b () String) 
(declare-fun ae () String) 
(declare-fun c () String)  
(declare-fun af () String) 
(declare-fun i () String)
(declare-fun j () String) 
(declare-fun ah () String) 
(declare-fun m () String) 
(declare-fun l () String)
(declare-fun q () String)   
(declare-fun n () String) 
(declare-fun s () String) 
(declare-fun r () String) 
(declare-fun aj () String) 
(declare-fun e () Bool) 
(declare-fun f () Bool)  
(declare-fun g () Bool)  
(declare-fun h () Bool) 
(declare-fun o () Bool) 
(declare-fun p () Bool) 
(assert (= e (not (= (/ a d) (- 1))) (= "" ( str.substr i 0 (str.len q)))(= f (not (= e o)))))    
(assert (ite (not (= h e)) (and (= k 0 (str.len ( str.substr b 0 (str.len j)))) (= ( str.substr ae 0 (str.len ah)) "" ( str.substr c 0 (str.len m)) l)) (and (=  0 (str.len ( str.substr b 0 (str.len j)))) (not ( str.in.re ae (str.to.re "=")))))) 
(assert (= (= g p) (not (= (/ a d)  1))(not (= h p)) (and  (= b ( str.++ (str.substr c (str.len m) (str.len n)) b )( str.++ s (str.substr b (str.len j) (str.len ( str.substr af 0 (str.len r))))))(not (= aj "")))))
(check-sat)