WyCS: Finally managed to get tests passing with Z3!!
WyC: Updated output for files
Merge branch 'master' of github.com:Whiley/WhileyCompiler
WyJC: Updated valid test cases.
A number of valid test cases were incorrectly marked as @Ignore when
they were in fact passing.  Some were additionally missing sample
output.
BUILD: Updated to latest version on Jasm.
The latest version of Jasm contains a bug fix related to the compilation
of functions containing a larger number of local variables.
WyC,WyIL,WyjC: Added an AssertBlock bytecode #377.
The purpose of this bytecode is as a stepping stone towards bytecode
blocks (#190).  Furthermore, to remove the e.g. assertge bytecodes, and
replace them with fail bytecodes.  This should reduce the number of path
generated during verification condition generation.
WyC: Deleted CodeGenerator.
This class represents the future.  Unfortunately, there are two many
pressing changes that I need to push through that I cannot maintain it.
Therefore, I'm deleting it and I will simply need to regenerate it from
the OldCodeGenerator at some point in the future.
WyC: Deleted CodeGenerator.
This class represents the future.  Unfortunately, there are two many
pressing changes that I need to push through that I cannot maintain it.
Therefore, I'm deleting it and I will simply need to regenerate it from
the OldCodeGenerator at some point in the future.
WyC,WyIL,WyJC: Added AssumeBlock Bytecode #377.
As part of the move towards bytecode blocks, and the use of fail inplace
of e.g. assertge bytecodes, I have implemented the AssumeBlock bytecode.
WyC,WyIL: Removed assertge and related bytecodes.
This is not yet finished, as I need to plumb through a number of other
important fixes to the CodeGenerator and related pieces.
Merge branch 'devel-assert' of github.com:Whiley/WhileyCompiler into devel-assert
WyC,WyIL,WyJC: Removed assertXX bytecodes #377.
These bytecodes are now replaced with Assert blocks and Fail bytecodes.
This transformation is not yet complete.  Specifically, I still need to:
a) fixup DecisionTree; b) put back in loop invariants and
pre/post-conditions; c) make sure inlined invariants are put into an
Assert block.
WyC: minor updates ahead of next release.
Merge pull request #413 from hjwylde/devel-smt

Pulling your changes.  Sorry they didn't make the latest release, but they'll be in v0.3.29, to be released next week!
Merge remote-tracking branch 'origin/devel-smt'

Conflicts:
	modules/wycs/src/wycs/solver/smt/Solver.java
	modules/wycs/src/wycs/solver/smt/Sort.java
	modules/wycs/src/wycs/transforms/SmtVerificationCheck.java
WyIL: Added enable flag for BackPropagation #416.
The BackPropagation phase did not have an enable flag, which seems
unsusual compared with other WyIL transforms.  Therefore, I've added
one!
Updated .gitignore to include smt2 files.
The smt2 files are generated by the SmtVerificationCheck phase, and
are only temporary files.
WyC: Added missing file.
Merge branch 'master' into devel-assert

Conflicts:
	modules/wyc/src/wyc/builder/FlowTypeChecker.java
WyCS: Improved Error Reporting #411.
When a resolution failure occured during MacroExpansion, there was no
proper error handling.  Instead, a NullPointerException was raised.
This was causing confusing errors in some cases.