debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
*	Small refactoring	Ally Donaldson	2014-06-06
\|
*	Merge duality changes	Ken McMillan	2014-05-26
\|\
\| *	Conjecture printing for duality and child user time tracking.	Ken McMillan	2014-05-26
\| \|
* \|	Simplify Z3 executable discovery.	wuestholz	2014-05-12
\|/
*	Added /printFixedPoint option	Ken McMillan	2014-04-14
\|
*	Fixed bug in printing real literals	Rustan Leino	2014-02-10
\|
*	Fix Boogie so it compiled with mono. Patch by Dan Liew.	Ally Donaldson	2014-01-14
\|
*	fixed vc generation so that even when builtin array functions are used,	qadeer	2013-12-28
\| \| \| \|	the program can be verified without the use of /useArrayTheory
*	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.
*	added the QED build configuration	qadeer	2013-12-02
\|
*	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
\| \|
* \|	ProverInterface: model isn't available on timeout	akashlal	2013-11-02
\| \|
* \|	small refactoring	Pantazis Deligiannis	2013-10-02
\| \|
* \|	changes to support a configured errorLimit	Pantazis Deligiannis	2013-09-30
\| \|
* \|	Merge	Pantazis Deligiannis	2013-08-20
\|\ \
* \| \|	new option to disable checking for loop maintained invariants - this leads ↵	Pantazis Deligiannis	2013-08-15
\| \| \| \| \| \| \| \| \| \| \| \|	to an underapproximation that helps to speedup houdini refutation of candidates
\| * \|	Reverted change to use MODEL_ON_FINAL_CHECK, which seems to cause Z3 ↵	Rustan Leino	2013-08-02
\| \| \| \| \| \| \| \| \| \| \| \|	unexpectedly to output model information
\| * \|	Turned on options in Z3 to try producing models for timeouts.	wuestholz	2013-08-02
\| \| \|
\| * \|	Removed harmful "Assert(false)".	wuestholz	2013-07-26
\|/ /
* \|	Resolved some issues with data races.	wuestholz	2013-07-23
\| \|
* \|	More refactoring	Ally Donaldson	2013-07-22
\| \|
* \|	small fix to pickup correctly the CVC4 executable	Pantazis Deligiannis	2013-07-22
\| \|
* \|	fix	Pantazis Deligiannis	2013-07-22
\| \|
* \|	refactoring	Pantazis Deligiannis	2013-07-22
\| \|
* \|	refactoring	Pantazis Deligiannis	2013-07-22
\| \|
* \|	merge	Pantazis Deligiannis	2013-07-19
\|\ \
* \| \|	refactoring and fixes in the SMTLIB2 parser	Pantazis Deligiannis	2013-07-19
\| \| \|
\| * \|	Revamp of staged Houdini, and completion of parallel support.	allydonaldson	2013-07-18
\| \| \|
* \| \|	fix: can now setup CVC4 logic properly, default is ALL_SUPPORTED, other ↵	Pantazis Deligiannis	2013-07-15
\| \| \| \| \| \| \| \| \| \| \| \|	logics can be set with the previously existing command e.g. /proverOpt:LOGIC=QF_ALL_SUPPORTED
* \| \|	fix for SetTimeOut in ProverInterface to work only under Z3 parser	Pantazis Deligiannis	2013-07-15
\| \| \|
* \| \|	small fix	Pantazis Deligiannis	2013-07-15
\| \| \|
* \| \|	Merge	Pantazis Deligiannis	2013-07-15
\|\ \ \ \| \|/ / \|/\| \|
\| * \|	temp fix until CVC4 bug is fixed (using QF_ALL_SUPPORTED instead of ↵	Pantazis Deligiannis	2013-07-15
\| \| \| \| \| \| \| \| \| \| \| \|	ALL_SUPPORTED)
\| * \|	code cleanup and refactoring	Pantazis Deligiannis	2013-07-11
\| \| \|
\| * \|	code cleanup & refactoring	Pantazis Deligiannis	2013-07-11
\| \| \|
* \| \|	Worked on the parallelization.	wuestholz	2013-07-10
\| \| \|
\| * \|	the cvc4 parser can now parse nested array expressions	Pantazis Deligiannis	2013-07-10
\| \| \|
\| * \|	fixed a bug where a formula was being send to CVC4 although it shouldn't ↵	Pantazis Deligiannis	2013-07-10
\| \| \| \| \| \| \| \| \| \| \| \|	normally
\| * \|	added specific command line options to enable the SMTLIB2 output model ↵	Pantazis Deligiannis	2013-07-09
\| \| \| \| \| \| \| \| \| \| \| \|	parser for Z3. Use /proverOpt:SMTLIB2_MODEL=true
\| * \|	some clean up	Pantazis Deligiannis	2013-07-09
\| \| \|
* \| \|	Worked on the parallelization.	wuestholz	2013-07-08
\| \| \|
\| * \|	allows (reset) to be send only to the Z3 prover	Pantazis Deligiannis	2013-07-09
\| \| \|
* \| \|	Worked on the parallelization.	wuestholz	2013-07-08
\| \| \|
\| * \|	merge	Pantazis Deligiannis	2013-07-06
\| \|\ \ \| \|/ / \|/\| \|
* \| \|	Worked on the parallelization.	wuestholz	2013-07-05
\| \| \|