util.analyzers
compute the SMT expression (exists e1..ek (c in1..inn e1..ek)=(o1..om)) in traceFieldExpr where flows are given as bounded variables referred in traceFieldVars
compute the SMT expression (exists e1..ek (c in1..inn e1..ek)=(o1..om)) in traceFieldExpr where flows are given as bounded variables referred in traceFieldVars