Trigger computation algorithm has unexpected effect on negative integer literals

[viper-admin]

Created by @mschwerhoff on 2014-08-31 18:52

Consider the following Silver snippet:

#!text

function fun(i: Int): Int
  requires i >= 0
{ i }

method test() {
  assert forall i: Int :: (i in Seq(-2,2,4,6,8)) ==> (fun(i*i) > i)
}

The version of the quantifier returned by the trigger computation algorithm (autoTrigger) is:

#!text
forall i: Int, fresh__1: Int ::
  { (i in Seq(fresh__1, 2, 4, 6, 8)) }
  i in Seq(-2, 2, 4, 6, 8) ==> fun(i * i) > i

In my opinion, the negative integer literal -2 should not have been replaced by a fresh, quantified variable.