BranchReasoning (gillian.Bulk.BranchReasoning)

val makeFormater : 
  (string -> string) ->
  (Stdlib.Format.formatter -> 'a -> unit) ->
  Stdlib.Format.formatter ->
  'a ->
  unit

type branches =

| ExactlyOne
| AllOfThem
| AtLeastOne

val build_message_all : 
  ?fmtexp:(string -> string) ->
  Gillian.Gil_syntax.Flag.t ->
  (string * 'a) option ->
  string list ->
  string

Builds a message explaining the reason of failure when the `AllOfThem` is used. In this case, it explained every case that didn't match the expected patternd

val oneResInMode : 
  ?fmtexp:(string -> string) ->
  ?fmtrcv:(string -> string) ->
  pp_what_branch_did:
    (Stdlib.Format.formatter -> ('a, 'b, 'c) Engine.Exec_res.t -> unit) ->
  Gillian.Gil_syntax.Flag.t ->
  (string * ('b -> 'a -> bool)) option ->
  ('a, 'b, 'c) Engine.Exec_res.t ->
  bool * string

val resInMode : 
  ?fmtexp:(string -> string) ->
  ?fmtrcv:(string -> string) ->
  pp_what_branch_did:
    (Stdlib.Format.formatter -> ('a, 'b, 'c) Engine.Exec_res.t -> unit) ->
  branches ->
  Gillian.Gil_syntax.Flag.t ->
  (string * ('b -> 'a -> bool)) option ->
  ('a, 'b, 'c) Engine.Exec_res.t list ->
  ('d -> string) * bool