Constant move_model::pragmas::CONDITION_ISOLATED_PROP

pub const CONDITION_ISOLATED_PROP: &str = "isolated";

Property which can be attached to a global invariant to mark it as not to be used as an assumption in other verification steps. This can be used for invariants which are nonoperational constraints on system behavior, i.e. the systems “works” whether the invariant holds or not. Invariant marked as such are not assumed when memory is accessed, but only in the pre-state of a memory update.