Conveniently, many of the mathematical lemmas we've proven in Libraries/Math/*.dfy have _forall variants that make them easy to invoke, like lemmamulisdistributiveforall(). Unfortunately, each of these _forall variants introduces a large number of potential facts, which may confuse Z3 and make it time out. This is particularly likely to happen for DafnyCC, so you should probably avoid using _forall lemmas in all but the shortest and simplest methods.

The reason DafnyCC tends to be worse than Dafny at this is as follows. Dafny gives you quick feedback about whether it can prove things in a timely fashion. So you'll generally try various strategies until you find one that works. DafnyCC does not provide such quick feedback, so you won't really have an opportunity to try too many strategies. So while there may be a strategy using a _forall that will avoid a timeout, you may hit a personal human-frustration timeout trying to find such a strategy.

Last edited Oct 15, 2014 at 12:13 AM by howell, version 1

Comments

No comments yet.