Trigger computation algorithm has unexpected effect on negative integer literals

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.

Reproduce the Silver snippet in the issue and inspect the autoTrigger implementation that transforms the quantified expression. Check how negative integer literals are handled when constructing trigger terms. Done means the generated trigger preserves -2 rather than replacing it with a fresh quantified variable, while the example still verifies correctly.