smt.seq.validate smt.phase_selection smt Non-deterministic segmentation fault with Seq

[muchang]

Hi,
For this formula:

(set-option :smt.seq.validate true)  
(set-option :smt.threads 3) 
(set-option :smt.phase_selection 5) 
(declare-fun s0 () (Seq Int)) 
(declare-fun s1 () Int) 
(declare-fun a () Int) 
(define-fun s7 () Int 172) 
(define-fun s8 () Bool (>= s1 s7)) 
(define-fun b () Bool s8) 
(define-fun c () Int (seq.nth s0 s1)) 
(define-fun d () Bool (= a c)) 
(define-fun s12 () Bool (or b d)) 
(define-fun s13 () Bool s12) 
(define-fun s14 () (Seq Int) (seq.unit a)) 
(define-fun s15 () Int (seq.indexof s0 s14)) 
(define-fun e () Bool (<= s15 s1)) 
(define-fun s17 () Bool (xor s13 e)) 
(assert s17)  
(check-sat-using  smt)     

Z3 throws out a segmentation fault:

$ ./z3/build/z3 small.smt2 
l_undef

(not (= (seq.prefix.y (seq.unit a) s0) (as seq.empty (Seq Int))))
(let ((a!1 (seq.++ (seq.prefix.x (seq.unit a) s0)
                   (seq.unit (seq.prefix.c (seq.unit a) s0))
                   (seq.prefix.y (seq.unit a) s0))))
  (= (seq.unit a) a!1))
Segmentation fault
$ ./z3/build/z3 small.smt2 
sat
$ ./z3/build/z3 small.smt2 
sat
$ cat small.smt2 
(set-option :smt.seq.validate true)  
(set-option :smt.threads 3) 
(set-option :smt.phase_selection 5) 
(declare-fun s0 () (Seq Int)) 
(declare-fun s1 () Int) 
(declare-fun a () Int) 
(define-fun s7 () Int 172) 
(define-fun s8 () Bool (>= s1 s7)) 
(define-fun b () Bool s8) 
(define-fun c () Int (seq.nth s0 s1)) 
(define-fun d () Bool (= a c)) 
(define-fun s12 () Bool (or b d)) 
(define-fun s13 () Bool s12) 
(define-fun s14 () (Seq Int) (seq.unit a)) 
(define-fun s15 () Int (seq.indexof s0 s14)) 
(define-fun e () Bool (<= s15 s1)) 
(define-fun s17 () Bool (xor s13 e)) 
(assert s17)  
(check-sat-using  smt) 

OS: Ubuntu 18.04
Commit: 65b2037

[NikolajBjorner]

smt.seq.validate is for internal debugging