debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
*	Improve support for identifying unnecessary assumes.	Valentin Wüstholz	2016-03-09
\|
*	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
\|
*	Enable optimization for more prover queries.	Valentin Wüstholz	2015-12-27
\|
*	Add experimental support for optimization (requires Z3 build after changeset ↵	Valentin Wüstholz	2015-11-18
\| \| \| \|	9cba63c31f6f1466dd4ef442bb840d1ab84539c7).
*	Add support for identifying unnecessary assumes.	Valentin Wüstholz	2015-11-16
\|
*	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.
*	removed a stray Console.WriteLine that Ken had earlier checked in by	qadeer	2015-06-25
\| \| \| \|	mistake.
*	Fix for reading fixpoint back into boogie exprs	akashlal	2015-06-20
\|
*	Fix minor issue with diagnosing timeouts.	Valentin Wüstholz	2015-06-12
\|
*	various changes for duality from dead codeplex repo	U-REDMOND\kenmcmil	2015-06-09
\|
*	Improve support for diagnosing timeouts.	Valentin Wüstholz	2015-06-08
\|
*	Improve support for diagnosing timeouts.	Valentin Wüstholz	2015-06-05
\|
*	Improve heuristics for diagnosing timeouts.	Valentin Wüstholz	2015-05-31
\|
*	Improve support for diagnosing timeouts.	Valentin Wüstholz	2015-05-22
\|
*	Minor changes	Valentin Wüstholz	2015-05-20
\|
*	Minor refactoring	Valentin Wüstholz	2015-05-20
\|
*	Improve support for diagnosing timeouts.	Valentin Wüstholz	2015-05-20
\|
*	Improve support for diagnosing timeouts.	Valentin Wüstholz	2015-05-19
\|
*	Add some experimental support for diagnosing timeouts.	Valentin Wüstholz	2015-05-18
\|
*	VC gen for security properties	akashlal	2015-04-05
\|
*	If using -proverLog: make sure we flush after writing every line	Dan Liew	2015-03-10
\| \| \| \| \| \| \| \| \|	otherwise if either of the following happens * if the solver hangs and we do CTRL+C * if Boogie crashes then some lines will be missing from the log.
*	Work around bug in Z3 4.3.2 and newer (https://z3.codeplex.com/workitem/188)	Dan Liew	2015-03-10
\| \| \| \| \| \|	where setting produce-unsat-cores to true has no effect unless the option is set last. This makes the Test/houdini/testUnsatCore.bpl test pass under Linux using Z3 4.3.2
*	Parse Bv values	akashlal	2015-03-02
\|
*	Merge some FixpointVC changes that got left behind	Ken McMillan	2014-12-08
\|\
* \|	Patch by Jeroen Ketema	Dan Liew	2014-11-17
\| \| \| \| \| \| \| \|	Fix interfacing with CVC4 1.5
* \|	re-enabling -useUnsatCoreForContractInfer	shuvendu	2014-11-07
\| \| \| \| \| \| \| \|	An example houdini\testUnsatCore.bpl to test out the unsatCore (Currently seems to be not working)
* \|	Logging for SMTLib prover	akashlal	2014-11-05
\| \|
\| *	Merge FixpointVC changes with mainline	Ken McMillan	2014-10-08
\|/\|
\| *	Added "extra recursion bound" to FixedpointVC to support Corral.	Ken McMillan	2014-10-08
\| \|
* \|	Some fixes to ITP	akashlal	2014-10-04
\| \|
* \|	minor fixes to interpolating TP	akashlal	2014-10-03
\| \|
* \|	Added a flag to initialize the interpolating TP	akashlal	2014-09-29
\| \|
* \|	Merge.	Dan Liew	2014-09-24
\|\ \
* \| \|	Remove dead method argument	Dan Liew	2014-09-24
\| \| \| \| \| \| \| \| \| \| \| \|	Patch by Jeroen Ketema
* \| \|	Let the SMT lib convert models to Z3-like models	Dan Liew	2014-09-24
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The Model parser for SMT models is broken beyond repair and this by-passes this. The code could be moved to the model parser, but that's a refactoring for another day. Also, the existing version already had multiple reparses going on and this at least removes one of those. Patch by Jeroen Ketema.
\| * \|	(Subhajit) Added an interface for InterpolatingTheoremProver	akashlal	2014-09-24
\| \| \|
\| * \|	Simple VC generation for SI	akashlal	2014-09-24
\|/ /
* /	Patch by Jeroen Ketema.	Dan Liew	2014-09-19
\|/ \| \| \| \| \|	Only set produce-unsat-cores in the case /explainHoudini is passed. This allows contract inference to be used with solvers that do no support unsat cores, as long as no explanation of the Houdini run is required.
*	OnModel now carries the result of the prover call	akashlal	2014-06-28
\|
*	Small refactoring	Ally Donaldson	2014-06-06
\|
*	Conjecture printing for duality and child user time tracking.	Ken McMillan	2014-05-26
\|
*	Added /printFixedPoint option	Ken McMillan	2014-04-14
\|
*	Merge	Ally Donaldson	2013-12-09
\|\
* \|	Small change related to CVC4 support. Patch by Pantazis Deligiannis	Ally Donaldson	2013-12-09
\| \|
\| *	The back pred files have been eliminated. The small backpred string is now ↵	qadeer	2013-12-08
\|/ \| \| \|	directly included in ProverInterface.cs.
*	do monomorphic checking	qadeer	2013-11-22
\|
*	Fixedpoint VC catch up with recent changes	Ken McMillan	2013-11-11
\|
*	Merge duality changes to mainline	Ken McMillan	2013-11-09
\|\
\| *	handling timeouts for fixedpoint engines	Ken McMillan	2013-11-09
\| \|