sig
  val eval_predicate :
    (pre:Db.Value.state ->
     here:Db.Value.state ->
     Cil_types.predicate -> Property_status.emitted_status)
    Pervasives.ref
end