Как правильно приостановить инвариантную проверку в Why3?

Question

Предположим, у меня есть следующий тип:

type example {
   mutable a : int
   mutable b : int
}
invariant { 
   a = b
}

Как я могу приостановить проверку инварианта, чтобы я мог выполнить операцию, которая нарушает инвариант?Такие как:

let add (t : example)(n : int) =
   t.a <- t.a + n
   t.b <- t.b + n