debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Minor corrections	akashlal	2014-10-01
\|
*	SI: VC gen with labels	akashlal	2014-09-29
\|
*	Cleanup: removed unused code	akashlal	2014-09-29
\|
*	Fix to VC gen	akashlal	2014-09-28
\|
*	Fix for boolVC generation	akashlal	2014-09-27
\|
*	Lets have a setter for TopLevelDeclarations as well	akashlal	2014-09-25
\|
*	minor fix	akashlal	2014-09-24
\|
*	Simple VC generation for SI	akashlal	2014-09-24
\|
*	Did more refactoring and addressed several todos.	wuestholz	2014-09-23
\|
*	Did some refactoring.	wuestholz	2014-09-23
\|
*	Bug fix in SI	akashlal	2014-08-03
\|
*	Some simplifications	akashlal	2014-07-28
\|
*	OnModel now carries the result of the prover call	akashlal	2014-06-28
\|
*	Fix in SI while dealing with timeouts	akashlal	2014-06-27
\|
*	keep some stats for debugging	akashlal	2014-05-15
\|
*	Added stack bounding	akashlal	2014-05-10
\|
*	Recursive walking of Exprs doesn't play nice when the depth of the AST is high.	akashlal	2014-01-07
\| \| \| \| \|	Reduce depth of AST whenever possible (e.g., use a binary tree instead of a linear list of terms)
*	code cleanup	akashlal	2013-11-02
\|
*	And a test case	akashlal	2013-10-21
\|
*	Bug fix in stratified inlining (triggered by {:inline} functions)	akashlal	2013-10-21
\|
*	Merge	Pantazis Deligiannis	2013-10-09
\|\
* \|	changes to support a configured errorLimit	Pantazis Deligiannis	2013-09-30
\| \|
\| *	refactored StratifiedInline.GenerateVC to use GenerateVCAux instead of ↵	qadeer	2013-09-09
\| \| \| \| \| \| \| \|	GenerateVC
\| *	Factored out the closure for codeexpr conversion so that it can be reused.	qadeer	2013-09-04
\|/ \| \| \|	Enabled it in stratified inlining.
*	Fixed several build errors in the 'Checked' configuration.	wuestholz	2013-08-05
\|
*	ExprSeq: farewell	Ally Donaldson	2013-07-22
\|
*	BlockSeq: farewell	Ally Donaldson	2013-07-22
\|
*	CmdSeq: farewell	Ally Donaldson	2013-07-22
\|
*	Started to remove ...Seq classes	Ally Donaldson	2013-07-22
\|
*	More refactoring	Ally Donaldson	2013-07-22
\|
*	More refactoring towards replacing PureCollections.Sequence with List	Ally Donaldson	2013-07-22
\|
*	merge	Pantazis Deligiannis	2013-07-22
\|\
\| *	Large refactoring of Hashtable to Dictionary.	Ally Donaldson	2013-07-22
\| \|
\| *	Refactored labsl2absy so that it is a Dictionary<int, Absy> instead of a ↵	Ally Donaldson	2013-07-22
\| \| \| \| \| \| \| \|	plain Hashtable.
* \|	merge	Pantazis Deligiannis	2013-07-06
\|\\|
\| *	Did some refactoring in the execution engine and worked on the parallelization.	wuestholz	2013-07-01
\| \|
* \|	merged more CVC4 and Z3 SMTLIB2 parsing methods ... results into a more ↵	pantazis	2013-06-13
\|/ \| \| \|	compact parser
*	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)
*	bunch of refactorings	Unknown	2012-10-03
\| \| \| \| \| \| \| \| \|	- moved doomed and predication code into separate projects; for doomed there is a static dependency from BoogieDriver but for predication even that dependency has been eliminated - deleted Provers\Simplify and Provers\Z3 - removed Provers\Z3api from the solution - consolidated Core\GraphAlgorithms.cs VCGeneration\GraphAlgorithms.cs into Graph\Graph.cs
*	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.
*	deleted an unused class	qadeer	2012-06-12
\|
*	refactoring in SI	qadeer	2012-06-12
\|
*	1. changed new SI implemnetation so that it performs substitution for call sites	qadeer	2012-06-10
\| \| \| \|	2. changed the block expression to be the negation of the disjunction of all outgoing edges
*	final (hopefully) fix to new SI	qadeer	2012-06-07
\|
*	testing a fix in SI	qadeer	2012-06-07
\| \| \| \| \|	also changing back the output path in BoogieDriver also disabling z3api for now since it does not build
*	Bug fix with mvInfo during VCGen	akashlal	2012-06-06
\|
*	update to SI	qadeer	2012-06-04
\|
*	moved class Macro to Absy	qadeer	2012-06-04
\| \| \| \| \|	cleanup up DefineMacro Changed SI to use macros for reach info
*	added FindLeastToVerify to StratfiedVCGenBase as an abstract method	qadeer	2012-05-30
\|