util.analyzers
compute the SMT expression (c in1..inn e1..ek)=(o1..om) where flows and events are bounded variables
compute the SMT expression (c in1..inn e1..ek)=(o1..om) where flows and events are bounded variables