Verifier (gillian.Engine.Verifier)

module type S = sig ... end

module Make
  (SState : 
    SState.S
      with type vt = Gillian.Symbolic.Values.t
       and type st = Gillian.Symbolic.Subst.t
       and type store_t = SStore.t)
  (SPState : 
    PState.S with type state_t = SState.t and type init_data = SState.init_data)
  (PC : Gillian.Command_line.ParserAndCompiler.S)
  (External : Engine.External.T(PC.Annot).S) : 
  S
    with type heap_t = SPState.heap_t
     and type m_err = SPState.m_err_t
     and type state = SPState.t
     and module SPState = SPState
     and type annot = PC.Annot.t