Integer multiplication errors

[echuber2]

Edit: The anomalous assertion below was found by @nishantjr. I would not have poked around at it had he not mentioned it first.

This assertion highlights strange behavior that may be due to the issues with non-linear arithmetic in general, and I can't tell if it's expected behavior, or a bug in Dafny, or a bug in Boogie.

Input program test2.dfy:

method foo(n:int)
{
 assert(((n*(n+1))/2) + ((n*(n+1))/2) == (n*(n+1)));
}

Going to try it with Dafny 2.2.0.10923, which is just what I was able to run conveniently using this docker on Docker Hub: ssaavedra/dafny However, it also fails (without showing a counterexample) if I run it with a more recent version of Dafny.

I get an assertion failure and no matter what options I use, it seems like the counterexample is always due to a simple mistake in multiplication. Let me show some invocations and excerpted output.

dafny test2.dfy /traceverify /pretty:1 /printModel:4 /arith:2

This shows this:

Mul -> {
  513 514 -> 262657
  else -> 262657
}

Now note that 513*514 should be 263682. Instead, this seems to match this expression:

((513-1)*(514-1)) + 1

which is 262657. And that's what seems to be implied by Boogie, here:

https://github.com/boogie-org/boogie/blob/044e533713346840b55e53c33082911fd077d299/Source/AbsInt/IntervalDomain.cs#L898

(I'm not even sure what Boogie is trying to achieve with that bounding interval, to be honest.) So, is this a bug in Boogie, or is Dafny translating it to Boogie incorrectly?

If I run it like this instead:

dafny test2.dfy /traceverify /pretty:1 /printModel:4 /arith:4

Then I get this:

Mul -> {
  (- 3) (- 2) -> (- 25)
  else -> (- 25)
}

Another run:

dafny test2.dfy /traceverify /pretty:1 /printModel:4 /noNLarith

Output:

INTERNAL_mul_boogie -> {
  (- 25) (- 24) -> 1451
  else -> 1451
}

You can generate other weird examples by adding non-failing assertions before the one I included, which seems to change the numbers seeded a bit.

So, is this a bug in Dafny or in Boogie, or am I overlooking something simple? Or must one define a replacement function for multiplication that unrolls into addition?

[davidcok]

Confirmed this problem.

[acioc]

We will revisit this after we've updated Dafny to the latest version of boogie and z3.