Failing arithmetic proofs (Z3)

[viper-admin]

Created by @mschwerhoff on 2017-03-31 13:32

Currently fails, most likely due to an incompleteness in Z3:

inhale 0 <= a && 0 <= b && 0 < n
inhale a * (n - 1) + b < |xs|
var i: int
inhale 0 <= i && i <= n - 1
assert a * i + b < |xs|

[fabiopakk]

This example is incomplete. @mschwerhoff could you please confirm the complete program is the following?

method m(a: Int, b: Int, n: Int, xs: Set[Int]){
  inhale 0 <= a && 0 <= b && 0 < n
  inhale a * (n - 1) + b < |xs|
  var i: Int
  inhale 0 <= i && i <= n - 1
  assert a * i + b < |xs|
}

The reported issue remains to this date.