Witness.Resultmodule R : ResultQuery.SpecSysSol2module Query : sig ... endmodule ArgTool : sig ... endmodule NHT = ArgTool.NHTmodule type BiArgInvariant = sig ... endval determine_result :
((MyCFG.node * R.SpecSys.Spec.C.t) * 'a) list ->
(module Svcomp.Task) ->
(module WitnessTaskResult)val write :
(Svcomp.Result.t, string) result option ->
((MyCFG.node * R.SpecSys.Spec.C.t) * 'a) list ->
unit