debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	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)
*	Boogie: internal clean-up, removed BvHandling type, everything now behaves ↵	Rustan Leino	2011-10-27
\| \| \| \|	as if the old /bv:z were used
*	Name the constant used in @MV_state function applications - otherwise we get ↵	Michal Moskal	2011-09-26
\| \| \| \|	invalid Z3 files
*	Fix contracts so runtime checking can be turned on.	mikebarnett	2011-03-07
\|
*	Boogie: Commented out all occurences of repeated inherited contracts - makes ↵	tabarbe	2010-08-27
\| \| \| \|	fewer error messages when compiling with runtime checking on.
*	Boogie: Removed an incorrect Ensures clause on a void method.	tabarbe	2010-08-27
\|
*	Chase type synonyms in arguments/results of map types when generating name ↵	MichalMoskal	2010-08-18
\| \| \| \|	(with tE:m).
*	Change Synonym type printing to what it was, use a workaround in ↵	MichalMoskal	2010-08-18
\| \| \| \|	TypeToString() instead. Add test for /typeEncoding:m.
*	Fix stack overflow introduced in my previous checkin. Make /typeEncoding:m ↵	MichalMoskal	2010-08-18
\| \| \| \|	use separate Z3 type per Boogie type
*	Boogie: Committing new source code for VCExpr	tabarbe	2010-08-13
\|
*	Boogie: Renaming VCExpr sources in preparation for port commit	tabarbe	2010-08-13