debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Fix issue with partially-verified assertions.	Valentin Wüstholz	2015-11-19
\|
*	Add a test.	Valentin Wüstholz	2015-11-16
\|
*	Add a test.	Valentin Wüstholz	2015-11-16
\|
*	Normalise line endings using a .gitattributes file. Unfortunately	Dan Liew	2015-06-28
\| \| \| \| \| \|	this required that this commit globally modify most files. If you want to use git blame to see the real author of a line use the ``-w`` flag so that whitespace changes are ignored.
*	Removed old test infrastructure files except for	Dan Liew	2014-05-28
\| \| \| \| \| \| \| \| \|	./AbsHoudini/ ./doomed/ ./z3api/ ./test17/ because their conversion to lit incomplete.
*	Fix lit test suite when running Boogie under a path that contains	Dan Liew	2014-05-27
\| \| \| \|	spaces.
*	Implemented an additional type check for assumption variables.	wuestholz	2014-05-27
\|
*	Remove old python testing scripts	Dan Liew	2014-05-11
\|
*	Enabled lit tests for test1/ directory	Dan Liew	2014-05-06
\| \| \| \|	Bizarely Array.bpl does not pass on Windows. This will be fixed soon.
*	Add support for assumption variables.	wuestholz	2014-04-21
\|
*	cleaned up the OG code	qadeer	2013-08-07
\| \| \| \|	enabled it to be always on
*	added python scripts (work in unix and windows) for testing Z3 and CVC4 to ↵	Pantazis Deligiannis	2013-07-07
\| \| \| \|	many of the test suite dirs
*	removed call forall and * args to calls	Unknown	2013-02-23
\|
*	Boogie and Dafny: adjustments to the test suite expected output (and a ↵	Unknown	2012-09-27
\| \| \| \|	temporary hack in FloydCycleDetect.dfy to be corrected shortly)
*	Boogie: added type 'real' with overloaded arithmetic operations plus real ↵	boehmes	2012-09-27
\| \| \| \| \| \| \| \| \|	division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
*	Split parts of AbsyExpr.ssc into AbsyQuant.ssc. Implement lambda ↵	MichalMoskal	2010-02-19
\| \| \| \|	expressions; they might not yet fully work for polymorphic maps.
*	Implement if-then-else expression.	MichalMoskal	2010-02-18
\|
*	Removed Output files. These are created on a local machine when the tests ↵	rustanleino	2009-08-07
\| \| \| \|	are run.
*	Initial set of files.	mikebarnett	2009-07-15