(set-option :smt.seq.validate true)   
(set-option :smt.phase_selection 5)  
(set-option :smt.threads 4)  
(declare-fun a () String) 
(declare-fun g () String) 
(declare-fun b () String) 
(declare-fun c () String) 
(declare-fun d () String)  
(declare-fun h () String) 
(declare-fun e () String)  
(declare-fun f () String)  
(assert (= (str.substr c 0 (str.len f)) (str.substr g 0 (str.len h)) (str.substr b 0 (str.len e )))) 
(assert (= (str.substr a 0 (str.len d)) "")) 
(check-sat)   

$ z3/build/z3 small.smt2 
l_undef

(let ((a!1 (str.++ (seq.unit (seq.nth d 0))
                   (str.substr d (+ 0 1) (- (str.len d) (+ 0 1))))))
  (not (= d a!1)))
(let ((a!1 (str.++ (seq.unit (seq.nth d 0))
                   (str.substr d (+ 0 1) (- (str.len d) (+ 0 1))))))
  (= d a!1))
Segmentation fault
$ z3/build/z3 small.smt2 
l_undef

(not (= e ""))
(let ((a!1 (str.++ (seq.unit (seq.nth e 0))
                   (str.substr e (+ 0 1) (- (str.len e) (+ 0 1))))))
  (not (= e a!1)))
Segmentation fault
$ z3/build/z3 small.smt2 
l_undef

(let ((a!1 (str.++ (seq.unit (seq.nth d 0))
                   (str.substr d (+ 0 1) (- (str.len d) (+ 0 1))))))
  (not (= d a!1)))
(let ((a!1 (str.++ (seq.unit (seq.nth d 0))
                   (str.substr d (+ 0 1) (- (str.len d) (+ 0 1))))))
  (= d a!1))
Segmentation fault
$ z3/build/z3 small.smt2 
l_undef

(not (= (seq.unit (seq.nth d 0)) (str.at d 0)))
(= (seq.unit (seq.nth d 0)) (str.at d 0))
Segmentation fault
$ z3/build/z3 small.smt2 
sat
$ z3/build/z3 small.smt2 
l_true

(let ((a!1 (str.++ (seq.unit (seq.nth h 0))
                   (str.substr h (+ 0 1) (- (str.len h) (+ 0 1))))))
  (not (= h a!1)))
(let ((a!1 (str.++ (seq.unit (seq.nth h 0))
                   (str.substr h (+ 0 1) (- (str.len h) (+ 0 1))))))
  (= h a!1))

(kernel)ASSERTION VIOLATION
File: ../src/smt/theory_seq.cpp
Line: 4678
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
A
$ cat small.smt2 
(set-option :smt.seq.validate true)   
(set-option :smt.phase_selection 5)  
(set-option :smt.threads 4)  
(declare-fun a () String) 
(declare-fun g () String) 
(declare-fun b () String) 
(declare-fun c () String) 
(declare-fun d () String)  
(declare-fun h () String) 
(declare-fun e () String)  
(declare-fun f () String)  
(assert (= (str.substr c 0 (str.len f)) (str.substr g 0 (str.len h)) (str.substr b 0 (str.len e )))) 
(assert (= (str.substr a 0 (str.len d)) "")) 
(check-sat)