debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	fixed some merging issues	Checkmate50	2016-06-07
\|
*	Improve support for identifying unnecessary assumes.	Valentin Wüstholz	2016-03-09
\|
*	Add support for weights on soft assumes.	Valentin Wüstholz	2016-03-07
\|
*	Improve support for optimization and identifying unnecessary assumes.	Valentin Wüstholz	2016-03-03
\|
*	Fix issue with ids for assume-statements.	Valentin Wüstholz	2015-12-28
\|
*	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.
*	Fix for printFixedPoint when dealing with functions	Akash Lal	2015-05-13
\|
*	Added /printFixedPoint option	Ken McMillan	2014-04-14
\|
*	More refactoring	Ally Donaldson	2013-07-22
\|
*	Worked on the parallelization.	wuestholz	2013-07-02
\|
*	Adding fixedpoint engine backend	Ken McMillan	2013-05-07
\|
*	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)
*	various changes for using unsat cores in Houdini	qadeer	2012-04-17
\|
*	more type checking for datatypes	qadeer	2012-03-18
\|
*	made delegate a datatype	qadeer	2011-12-30
\| \| \| \|	added a DatatypeConstructor class
*	fixed problems with datatypes	qadeer	2011-12-29
\| \| \| \| \|	removed stale contracts in stratified inlining added test to datatypes
*	Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)	Unknown	2011-10-19
\|
*	implementing datatypes	qadeer	2011-10-05
\|
*	Replaced all dictionaries that mapped to bool (i.e., were being used to ↵	mikebarnett	2011-03-10
\| \| \| \|	implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null.
*	Add MULTI_TRACES prover option (equivalent of /z3multipleErrors)	MichalMoskal	2011-02-23
\|
*	Don't try to declare bv types	MichalMoskal	2011-02-23
\|
*	Fixes in /useArrayTheory handling	MichalMoskal	2011-02-23
\|
*	Handle /useArrayTheory	MichalMoskal	2011-02-18
\|
*	Handle bitvectors	MichalMoskal	2011-02-18
\|
*	Use explicit mechanism for skipping to the next assertion	MichalMoskal	2011-02-17
\|
*	Bugfixes in select-of-store axioms	MichalMoskal	2011-02-16
\|
*	Use SMT2 top-level syntax	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
\|
*	Make the SMTLIB backend work again, particularly with /typeEncoding:m	MichalMoskal	2011-01-19
\|
*	Boogie: Fixed some doubly-inherited-contract occurrences.	tabarbe	2010-08-20
\|
*	Boogie: Committing my port of the SMTLib project	tabarbe	2010-07-22
\|
*	Boogie: Renaming the source files for the SMTLib project in preparation for ↵	tabarbe	2010-07-22
	commiting my port of the project.