debian-boogie - Debian packaging for Boogie

	Commit message (Expand)	Author	Age
*	Changed the syntax reading of the float type	Checkmate50	2016-07-16
*	Merging complete. Everything looks good crosses fingers	Checkmate50	2016-06-06
*	modified floating point syntax and modified floating point constants to use b...	Checkmate50	2016-03-17
*	Modified BigFloat and parser to accept correct SMT-LIB syntax	Checkmate50	2016-02-20
*	Special fp types (such as infinity and NaN are now translated by boogie	Checkmate50	2015-11-29
*	Modified translation so that z3 runs with type checking for simple binary ope...	Checkmate50	2015-10-14
*	Modified BigFloat to avoid evaluating the floating point value before sending...	Checkmate50	2015-09-23
*	Float type now works correctly for simple variable declaration and comparison.	Dietrich	2015-07-20
*	Modified internal abstract float representation to allow user-defined mantiss...	Dietrich	2015-07-13
*	integrated the named float type to act as a real in boogie	Dietrich	2015-05-04
*	Began adding the float type to VC expression	Dietrich	2015-04-27
*	more work on reducing call stack consumption	qadeer	2014-12-18
*	patched two occurrences of StackOverflowException on benchmarks from IronClad	qadeer	2014-12-16
*	Fix nasty bug introduced by commit 61a94f409975.	Dan Liew	2014-07-15
*	Fixed bug in printing real literals	Rustan Leino	2014-02-10
*	fixed vc generation so that even when builtin array functions are used,	qadeer	2013-12-28
*	Adding fixedpoint engine backend	Ken McMillan	2013-05-07
*	added support for linear sets without useArrayTheory (but there is some incom...	Unknown	2013-03-07
*	Boogie: added type 'real' with overloaded arithmetic operations plus real div...	boehmes	2012-09-27
*	Implement support for alternative SMT solvers -- CVC3 and CVC4	Peter Collingbourne	2012-09-06
*	Get Boogie and GPUVerify to compile and run with Mono	Peter Collingbourne	2012-05-02
*	fixed problems with datatypes	qadeer	2011-12-29
*	Fixed the generation of names for datatype functions to use the API for	Mike Barnett	2011-10-31
*	added membership tests	qadeer	2011-10-05
*	implementing datatypes	qadeer	2011-10-05
*	check in support for generalized array theory	Unknown	2011-09-06
*	Fix printing of (Array ...) types with /useArrayTheory	Michal Moskal	2011-09-06
*	Support multi-dimensional arrays in SMTLib2 backend (using Z3 extension though)	Michal Moskal	2011-09-06
*	further fixes; temporarily commented out	qadeer	2011-09-03
*	adding support for accessing Z3's generalized array theory	qadeer	2011-09-02
*	Use SMT2 syntax for sign_extend	Michal Moskal	2011-08-22
*	Use (get-model) Z3 command; quote skolem-ids	Michal Moskal	2011-04-28
*	Updates for the latest changes in Z3's SMT2 parser	Michal Moskal	2011-04-22
*	Use new, SMT2 compliant, Z3 syntax for labels	MichalMoskal	2011-04-02
*	Don't ever put a label under a quantifier.	MichalMoskal	2011-02-23
*	Add MULTI_TRACES prover option (equivalent of /z3multipleErrors)	MichalMoskal	2011-02-23
*	Add hack for {:bvbuiltin "sign_extend 42"}, which requires slightly different...	MichalMoskal	2011-02-23
*	Strip (= 0) and (!= 0) from patterns (we used to allow that with anyNeq thing...	MichalMoskal	2011-02-23
*	Fixes in /useArrayTheory handling	MichalMoskal	2011-02-23
*	Pass :skolemid to SMTLib prover	MichalMoskal	2011-02-23
*	Handle /useArrayTheory	MichalMoskal	2011-02-18
*	Remove workaround for Z3 scanner problems (fixed now); fix one comment	MichalMoskal	2011-02-18
*	Handle bitvectors	MichalMoskal	2011-02-18
*	Use explicit mechanism for skipping to the next assertion	MichalMoskal	2011-02-17
*	Fix printing of type-proxies	MichalMoskal	2011-02-16
*	Fix let scoping	MichalMoskal	2011-02-15
*	Use the new UniformArguments property; formatting	MichalMoskal	2011-02-15
*	Print terms in SMT2 syntax (drop term/formula distinction)	MichalMoskal	2011-02-15
*	Move name-quoting (already for SMT2 not SMT1) into a seprate class	MichalMoskal	2011-02-15
*	Add USE_PREDICATES option to TPTP and SMT provers	MichalMoskal	2011-02-11