summaryrefslogtreecommitdiff
path: root/Source/Provers/Z3/Prover.cs
Commit message (Collapse)AuthorAge
* bunch of refactoringsGravatar Unknown2012-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: internal clean-up, removed BvHandling type, everything now behaves ↵Gravatar Rustan Leino2011-10-27
| | | | as if the old /bv:z were used
* deleted lazyinlining option 2 and 3Gravatar qadeer2011-08-17
| | | | fixed proc copy bounding
* Update the RECENT_Z3 #define to include SORT_AND_ORGravatar Michal Moskal2011-06-30
|
* Renamed NonNullElements to NonNullDictionaryAndValues because the keys to ↵Gravatar mikebarnett2011-03-10
| | | | | | dictionaries are non-null, which is enforced by the implementation of Dictionary. Added class constraints to all of the generic NonNull and NonNullElements methods so only non-value types will be checked.
* Allow recent Z3 versions to be usedGravatar MichalMoskal2011-02-21
|
* Move model printing to ErrorModel classGravatar MichalMoskal2011-02-21
| | | | Allow construction of ErrorModel instance from Model instance
* Make the -mv option use the new Model class.Gravatar MichalMoskal2010-10-12
|
* Boogie:Gravatar rustanleino2010-10-12
| | | | | | * enhanced the printing of captured states * addressed some warnings issued by VS 2010 * some code formatting
* Boogie:Gravatar rustanleino2010-09-24
| | | | | * Added Test/textbook/DivMod.bpl, which embodies a conversion between C's div/mod operators and SMT Lib's div/mod operators. * Added a rudimentary printing of variables for captured states. It doesn't attempt to print everything at this time, and it doesn't work when variables get unique-ified by @@-suffixes. A more complete implementation will be added at a later time.
* Boogie:Gravatar rustanleino2010-09-23
| | | | | | * Added /mv flag as the start of a Boogie replacement for /cev * Allow attributes on assume statements * /mv looks for the assume-statement attribute :captureState with a string-literal argument
* Boogie: Commented out all occurences of repeated inherited contracts - makes ↵Gravatar tabarbe2010-08-27
| | | | fewer error messages when compiling with runtime checking on.
* Report a bug in Z3 instead of evil input "?"Gravatar kyessenov2010-08-23
|
* Boogie: Removed a completed task comment, added a forgotten ↵Gravatar tabarbe2010-08-19
| | | | Contract.EnsuresOnThrow<>()
* Remove -z3DebugTraces and -z3Mam options (no longer working). Rename the ↵Gravatar MichalMoskal2010-08-06
| | | | -z3bv option to Z3-specific -proverOpt:OPTIMIZE_FOR_BV=true. Start with the prover-specific help (still needs changes in the yet-unconverted part).
* Boogie: added /z3bv option that overrides the current setting of Z3 options ↵Gravatar stobies2010-08-06
| | | | for better performance on VCs that are heavy on bitvector arithmetic
* Remove support for Z3 V1 and clean up parameter processing code for Z3Gravatar stobies2010-08-06
| | | | svn-ignoring some build artifacts
* Boogie: cleanup option handling code for Z3Gravatar stobies2010-08-05
|
* Boogie: Removed trailing spaces in codeGravatar tabarbe2010-08-04
|
* Boogie: Committing ported version of Z3.Gravatar tabarbe2010-07-20
|
* Boogie: Let's try that rename again, shall we?Gravatar tabarbe2010-07-20
|
* Boogie: Rename didn't work. Resetting to try againGravatar tabarbe2010-07-20
|
* Boogie/Z3: Renaming the sources for Z3 in preparation for commit of my port ↵Gravatar tabarbe2010-07-20
of the project.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 10:05:15 +0000