Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
This is the result of running ./test.sh > `testresults` on HEAD, and can be used for very rudimentary regression testing if it is updated to reflect sound changes in output (new examples, optimisations, etc). Rumours of the last commit being unsound are greatly exaggerated. The false alarm was caused by the difference between the last time I ran test.sh and this time---during which Matt P. removed some unnecessary powersetting in the postcondition! The changes in output are due to this (theoretically sound) change. Hopefully this, and future regression test improvements, can fix this.
- Loading branch information