debian-boogie - Debian packaging for Boogie

	Commit message (Collapse)	Author	Age
...
\| * \|	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.
*	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
*	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.
*	Removed abandoned Isabelle prover backend	boehmes	2012-09-27
\|
*	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
*	Trying to merge with recent changes, failing.	Ken McMillan	2012-06-05
\|\
\| *	Some changes to support expanded use of z3api.	Ken McMillan	2012-06-05
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Should not affect function of other provers. There is an option added in Check.cs to allow creation of a Checker with a user-specified ProverContext. Also, some extension of z3api prover context to support conversion of Z3 formulas back to VCExpr. Finally, some experimental code, not enabled, to allow conversion of loops to recursion with "head recursion" rather than "tail recursion" (i.e., recursive call before loop body rather than after).
* \|	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
\|/ /
* \|	more type checking for datatypes	qadeer	2012-03-18
\| \|
* \|	bug fix	qadeer	2012-02-29
\| \|