If statement triggers

[dewert99]

I did notice that Viper removes if's with empty bodies causing some strange behaviour with triggers eg:

domain MyInt {
  function succ(n: MyInt): MyInt
  function pred(n: MyInt): MyInt

  axiom ps{
    forall n:MyInt :: 
      { pred(succ(n)) }
        pred(succ(n)) == n
  }
}

method test(n: MyInt, m: MyInt)
requires succ(n) == succ(m) 
ensures n == m {
  if (pred(succ(n)) != n) {
    assume true // Removing this line will cause an error 
  }
}