Skip to main content

ic3

logicaffeine_verify::ic3

Function ic3 

Source 
pub fn ic3(
    init: &VerifyExpr,
    transition: &VerifyExpr,
    property: &VerifyExpr,
    max_frames: u32,
) -> Ic3Result
Expand description

Run IC3/PDR on a safety property.

  • init: Initial state predicate (using @0 variables)
  • transition: Transition relation (using @t and @t1 variables)
  • property: Safety property to verify (using @t variables)
  • max_frames: Maximum number of frames before giving up