Not deterministic SMT query string

[pgarba]

Hi,

I noticed that some of the generated SMT queries have a different form when they are generated between several runs on the same LLVM IR. This leads to a cache miss and slows down the processing of the IR.

Do you know the reason for that ? Is it because of the PHIs ?!

Here is an example of the SMT queries for the same input LLVM IR:

; (Or (Eq false (And (And (And (And (And (Eq 1532383599 (Or w32 N0:(Read w32 0 arr) 1532383599)) (Eq 1532383598 (And w32 N0 1532383598))) (Eq false (Eq 0 N0))) (Sle 0 N0)) (And (Ult N0 1532383600) (Ule 1532383598 N0))) (And (And (Or (Eq false (Extract 0 (AShr w32 N0 31))) (Extract 0 (AShr w32 N1:(Add w32 2762583705 N0) 31))) (And (Eq (LShr w64 N2:(Shl w64 N3:(ZExt w64 N1) 3) 3) N3) (Eq (AShr w64 N2 3) N3))) (And (Or (Eq false (Extract 0 (AShr w64 (Add w64 4249920 N2) 63))) (Extract 0 (AShr w64 N2 63))) (Eq false (Extract 0 (AShr w65 (Add w65 4249920 (ZExt w65 N2)) 64))))))) (Eq 56 N2))

; (Or (Eq false (And (And (And (And (And (Eq 1532383599 (Or w32 N0:(Read w32 0 arr) 1532383599)) (Eq 1532383598 (And w32 N0 1532383598))) (Eq false (Eq 0 N0))) (Sle 0 N0)) (And (Ult N0 1532383600) (Ule 1532383598 N0))) (And (And (And (Or (Eq false (Extract 0 (AShr w64 (Add w64 4249920 N1:(Shl w64 N2:(ZExt w64 N3:(Add w32 2762583705 N0)) 3)) 63))) (Extract 0 (AShr w64 N1 63))) (Eq false (Extract 0 (AShr w65 (Add w65 4249920 (ZExt w65 N1)) 64)))) (And (Eq (LShr w64 N1 3) N2) (Eq (AShr w64 N1 3) N2))) (Or (Eq false (Extract 0 (AShr w32 N0 31))) (Extract 0 (AShr w32 N3 31)))))) (Eq 56 N1))

[regehr]

please share a souper command + input that makes this happen