Soundness bug on QF_SLIA formula with smt.arith.random_initial_value and 3 threads

[muchang]

Hi,
For this formula:

(set-option :smt.arith.random_initial_value true)  
(set-option :smt.threads 3)   
(declare-fun a () String)  
(declare-fun b () Int)  
(assert (<= b 72))  
(assert (=  (int.to.str b)  (str.++ "0" a)))  
(assert (distinct a ""))  
(check-sat)    

Z3 gives an incorrect answer:

$ z3debug/build/z3 small.smt2 
unsat
$ z3/build/z3 small.smt2 
sat
$ cat small.smt2 
(set-option :smt.arith.random_initial_value true)  
(set-option :smt.threads 3)   
(declare-fun a () String)  
(declare-fun b () Int)  
(assert (<= b 72))  
(assert (=  (int.to.str b)  (str.++ "0" a)))  
(assert (distinct a ""))  
(check-sat)

z3debug is correct.

OS: Ubuntu 18.04
Commit: f158ab8

[NikolajBjorner]

see bug 42

[NikolajBjorner]

#3430