Upgrading Boogie makes SystemTests fail to terminate

[l-kent]

Upgrading my Boogie installation from 2.16.0 to the latest version (3.0.4) has caused issues for the SystemTests - many tests now do not terminate.

We should standardise Z3 and Boogie versions to prevent any inconsistencies in the future. I am unsure which is best - Boogie 2.16.0 does not manage to verify the cntlm example with Nick's additions while 3.0.1 and above seem to be much more prone to failing to terminate, which is not desirable. I haven't tested any intermediate versions of Boogie. I have been using Z3 4.8.8 as that is recommended by Boogie (although there may be benefits to another version).

More immediately, adding time limits to the Boogie execution in the tests will at least force the tests to terminate.

It would have been helpful if someone had posted an issue for the termination problems previously - I was completely unaware of this being a problem until @ailrst mentioned termination issues yesterday.

[ailrst]

I've also found this to be the case for boogie 3.0.4 both with new z3 and z3 4.8.8. It does seem slightly better with z3 4.8.8.

[l-kent]

With z3 4.12.2 do more tests fail to terminate than with 4.8.8?

[l-kent]

Basic time limit added here: #80 but I'll still look at cleaning up the tests and testing various versions of Boogie to see if any seems to be most suitable.

[l-kent]

Nick has determined this is due to Boogie changing the default array theory to be the SMT theory of arrays instead of Boogie's axiom-based arrays implementation. This change happened with Boogie version 2.16.18. The SMT theory of arrays seems to perform much worse for us and have less success at verifying our examples, so we should use the /useArrayAxioms flag as a default.