debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	merge	Pantazis Deligiannis	2013-07-06
\|\
\| *	Worked on the parallelization.	wuestholz	2013-07-05
\| \|
\| *	Worked on the parallelization.	wuestholz	2013-07-02
\| \|
\| *	Worked on the parallelization.	wuestholz	2013-07-01
\| \|
\| *	fixed bad merge	Ken McMillan	2013-06-15
\| \|
\| *	Merge fixes for duality	Ken McMillan	2013-06-14
\| \|\
\| \| *	Fixes for duality under corral	Ken McMillan	2013-06-14
\| \| \|
* \| \|	fixed the CVC4 SMTLIB array parsing to work under the latest CVC4 model ↵	pantazis	2013-06-13
\| \| \| \| \| \| \| \| \| \| \| \|	representation changes
* \| \|	merged more CVC4 and Z3 SMTLIB2 parsing methods ... results into a more ↵	pantazis	2013-06-13
\| \| \| \| \| \| \| \| \| \| \| \|	compact parser
* \| \|	Z3 new parser takes now a new option for pp-bv-literals	pantazis	2013-06-12
\| \| \|
* \| \|	naive SMTLIB2 Parser	pantazis	2013-06-12
\| \| \|
* \| \|	CVC4 Parser	pantazis	2013-06-12
\| \| \|
* \| \|	cvc4 command line option & cvc4.cs in Provers	pantazis	2013-06-12
\|/ /
* \|	Fixed an issue in the prover interface.	wuestholz	2013-06-07
\| \|
* \|	Changed the prover interface to report traces for time outs and out of memory.	wuestholz	2013-05-30
\| \|
* \|	Minor change to prevent prover errors during trace extraction	wuestholz	2013-05-29
\|/
*	Adding background model to fixedpoint counterexamples and small code ↵	Ken McMillan	2013-05-29
\| \| \| \|	contracts fixes
*	Getting fixed point backend to work with Corral.	Ken McMillan	2013-05-29
\|
*	Working on fixedpoint backend	Ken McMillan	2013-05-20
\|
*	Adding fixedpoint engine backend	Ken McMillan	2013-05-07
\|
*	added support for linear sets without useArrayTheory (but there is some ↵	Unknown	2013-03-07
\| \| \| \|	incompletness)
*	fixed datatype bug reported by Chris	Unknown	2013-03-05
\| \| \| \|	fixed function body referring to globals bug
*	Parse integers returned by Z3 into BigNum	akashlal	2013-01-29
\|
*	Use the new ProverInterface's Evaluate method in stratified inlinig	Unknown	2013-01-03
\| \| \| \|	(guarded by the flag /useProverEvaluate)
*	bug fix	Unknown	2012-12-28
\|
*	extended Evaluate to handle more types	Unknown	2012-12-28
\|
*	Added expression evaluation API	Unknown	2012-12-27
\|
*	Bug fix for ExplainHoudini. Made it robust under timeouts.	Unknown	2012-12-20
\|
*	Incorporated contribution 3667, which fixes bug in /z3exe flag ↵	Rustan Leino	2012-11-20
\| \| \| \|	(http://boogie.codeplex.com/SourceControl/network/forks/stefanheule/boogiez3exefix/contribution/3667)
*	Fix for parsing error in MAXSAT computation in ↵	Unknown	2012-10-08
\| \| \| \|	ProverInterface::CheckAssumptions.
*	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)
*	Removed AIFramework from Boogie -- use native trivial or native ↵	boehmes	2012-09-27
\| \| \| \| \| \| \|	interval-based abstract interpretation instead. Command-line option '/infer' now accepts only arguments 't' and 'j' where the latter is the default now for Boogie. Command-line option '/logInfer' has been dropped.
*	Implement support for alternative SMT solvers -- CVC3 and CVC4	Peter Collingbourne	2012-09-06
\|
*	Made error trace generation (without labels) more general for stratified	Unknown	2012-07-04
\| \| \| \|	inlining
*	moved class Macro to Absy	qadeer	2012-06-04
\| \| \| \| \|	cleanup up DefineMacro Changed SI to use macros for reach info
*	Z3: do not assert that the ProgramFiles environment variable is set	Peter Collingbourne	2012-05-02
\| \| \| \| \|	This prevents mysterious exceptions from being thrown on platforms where ProgramFiles is not set.
*	Get Boogie and GPUVerify to compile and run with Mono	Peter Collingbourne	2012-05-02
\|
*	clean up in stratified inlining	qadeer	2012-04-29
\|
*	eliminated class ErrorModel	qadeer	2012-04-28
\|
*	removed proccopybounding code	qadeer	2012-04-28
\| \| \| \|	stratified inliinig is now run always with /doNotUseLabels
*	removed lazy inlining	qadeer	2012-04-28
\|
*	various changes for using unsat cores in Houdini	qadeer	2012-04-17
\|
*	small fix	qadeer	2012-04-04
\| \| \| \|	added regressions
*	added nonUniformUnfolding option	qadeer	2012-04-03
\|
*	deleted the option UseUnsatCoreForInlining	qadeer	2012-04-02
\| \| \| \| \|	Split ApiChecker.CheckAssumptions into two different methods, one which computes the unsatCore and one which does not Further edits to the MaxSat code
*	Merge	qadeer	2012-04-01
\|\
\| *	bug fix for previous refactoring	Unknown	2012-04-02
\| \|
* \|	Merge	qadeer	2012-04-01
\|\\|
* \|	partial work on non-uniform loop unrolling	qadeer	2012-04-01
\| \|
\| *	Refactored CheckAssumptions API	Unknown	2012-04-02
\|/