sig
  type prop_status =
      PropUnknown
    | PropKTrue of int
    | PropInvariant of Certificate.t
    | PropFalse of (StateVar.t * Model.value list) list
  type t = {
    prop_name : string;
    prop_source : Property.prop_source;
    prop_term : Term.t;
    mutable prop_status : Property.prop_status;
  }
  and prop_source =
      PropAnnot of Lib.position
    | Generated of StateVar.t list
    | Instantiated of Scope.t * Property.t
    | Assumption of Lib.position * string list
    | Guarantee of (Lib.position * Scope.t)
    | GuaranteeOneModeActive of (Lib.position * Scope.t)
    | GuaranteeModeImplication of (Lib.position * Scope.t)
    | Candidate of Property.prop_source option
  val pp_print_prop_source : Format.formatter -> Property.prop_source -> unit
  val pp_print_prop_status : Format.formatter -> Property.prop_status -> unit
  val pp_print_prop_quiet : Format.formatter -> Property.t -> unit
  val pp_print_property : Format.formatter -> Property.t -> unit
  val prop_status_known : Property.prop_status -> bool
  val set_prop_status : Property.t -> Property.prop_status -> unit
  val set_prop_invariant : Property.t -> Certificate.t -> unit
  val set_prop_ktrue : Property.t -> int -> unit
  val set_prop_false :
    Property.t -> (StateVar.t * Model.value list) list -> unit
  val length_of_cex : (StateVar.t * Model.value list) list -> int
  val get_prop_status : Property.t -> Property.prop_status
end