Slow verification of programs combining multiple floating point values

[classner]

(This is a re-post of my comment to PR #107, as requested by @zvonimir to streamline the discussion here.)

Hi!

I just found the floating point syntax update for Boogie and am very interested in it! Thanks for pushing this! :)

I just checked out the liammachado:improved_fp_syntax branch to play around with the FP implementation a bit. For examples combining two floating point values, the verification takes very long (so long I usually have to kill it early), e.g.:

procedure Exp1(a: float24e8, b:float24e8)
{
  var res: float24e8;
  assume(a > 0x1.0e0f24e8);
  assume(a < 0x4.0e5f24e8);
  assume(b > 0x1.0e0f24e8);
  assume(b < 0x4.0e5f24e8);
  res := a + b;
  assert(res > a);
  return;
}

Is that normal and intended? When using z3 directly to verify this using its FP syntax, it terminates very quickly.

[liammachado]

I don't think that PR #107 is causing this issue, since it also takes a long time to verify when I run this example on the master branch.

[zvonimir]

Ok, so let me comment on this. Thanks for reporting @classner, we certainly appreciate any feedback on our floating-point implementation.
I believe what you are observing here is the effect of theory combination on Z3, since we observed similar behaviors in the past. Basically, it seems that the theory of floating-points performs much better when your query is exclusively in that theory, instead of also involving things such as uninterpreted functions, arrays, etc.
Now, if you run Boogie on your example and use /proverLog:test.smt, you will likely notice that the generated query contains more than just pure floating-points, and at the very least it will contain uninterpreted functions. At least I think so.
On the other hand, I suspect that your direct encoding into Z3 was purely in the theory of floating-points.
This difference in the theories used could explain the discrepancy in the rutimes, at least based on our experience.
We have been looking into using Z3 tactics to get around this problem, but we still did not get to the bottom of this completely.
I hope this helps. Thoughts?

[bkragl]

The current version of Boogie (2.5.10) verifies the above example in (essentially) no time.