Execute (soteria-c.Soteria_c_lib.Summary.Execute)

val produce_atom : 
  State.syn Logic.Asrt.atom ->
  State.t option ->
  State.t option Csymex.CSYMEX.Producer.t

val produce : 
  State.syn Logic.Asrt.t ->
  State.t option ->
  State.t option Csymex.CSYMEX.Producer.t

val subst_covers : 
  Csymex.CSYMEX.Value.Expr.Subst.t ->
  Csymex.CSYMEX.Value.Expr.t ->
  bool

val ins_outs : 
  State.syn Logic.Asrt.atom ->
  Csymex.CSYMEX.Value.Expr.t list * Csymex.CSYMEX.Value.Expr.t list

val is_consumable : 
  Csymex.CSYMEX.Value.Expr.Subst.t ->
  State.syn Logic.Asrt.atom ->
  bool

val consume_atom : 
  State.syn Logic.Asrt.atom ->
  State.t option ->
  (State.t option, State.syn list) Csymex.CSYMEX.Consumer.t

val consume : 
  State.syn Logic.Asrt.t ->
  State.t option ->
  (State.t option, State.syn list) Csymex.CSYMEX.Consumer.t