summaryrefslogtreecommitdiff
path: root/Source/VCGeneration/Check.cs
Commit message (Expand)AuthorAge
* Use DateTime.UtcNow instead of DateTime.NowGravatar stobies2012-01-11
* Dafny: fixed bad Code ContractsGravatar Rustan Leino2011-11-16
* Eliminated unused argument in the constructor for CheckerGravatar qadeer2011-11-16
* change in model parsing with datatype valuesGravatar qadeer2011-11-07
* Boogie: Get rid of {:inline} attributes on axiomsGravatar Michal Moskal2011-10-27
* Boogie: internal clean-up, removed BvHandling type, everything now behaves as...Gravatar Rustan Leino2011-10-27
* Boogie: Eliminated the /bv option. Only native bitvectors are supported now. ...Gravatar Rustan Leino2011-10-27
* Added a push+pop+unsat-core interface to SMTLib (for stratified inlining only)Gravatar Unknown2011-10-19
* Options.PostParse() is called by Parse(), so set command-line-derived options...Gravatar Michal Moskal2011-08-30
* Add a string for an uninterpreted value in errModelGravatar Unknown2011-06-06
* Bug fix with model generation.Gravatar akashlal2011-03-21
* Renamed NonNullElements to NonNullDictionaryAndValues because the keys to dic...Gravatar mikebarnett2011-03-10
* Updated PrepareBoogieZip.bat to include BVD and smt2Gravatar rustanleino2011-03-10
* Handle as-array[...] model elementsGravatar MichalMoskal2011-02-23
* Parse else-> clauses in the modelGravatar MichalMoskal2011-02-23
* Throw exceptions when push/pop interface is used but not implementedGravatar MichalMoskal2011-02-23
* Move model printing to ErrorModel classGravatar MichalMoskal2011-02-21
* Allow use ErrorModel as a container for Model - make -mv work with SMTLib on Z3Gravatar MichalMoskal2011-02-18
* Get rid of -smtOutput option. Add /proverOpt:OUTPUT=... to SMT and TPTP prove...Gravatar MichalMoskal2011-02-11
* implemented /UseUnsatCoreForInlining option for use in stratified inliningGravatar qadeer2011-02-06
* Added CheckAssumptions api interfaceGravatar akashlal2010-11-28
* Some changes to the prover interface to make way for z3-api.Gravatar akashlal2010-11-24
* ModelViewer:Gravatar rustanleino2010-11-02
* Make the -mv option use the new Model class.Gravatar MichalMoskal2010-10-12
* Add the new model interface. Untested, doesn't yet include state sequenceGravatar MichalMoskal2010-10-08
* Get rid of some CCI dependencies in DriverGravatar MichalMoskal2010-10-07
* Boogie:Gravatar rustanleino2010-09-23
* Boogie: Commented out all occurences of repeated inherited contracts - makes ...Gravatar tabarbe2010-08-27
* Boogie: Fixed some doubly-inherited-contract occurrences.Gravatar tabarbe2010-08-20
* Boogie: Removed and completed a task commentGravatar tabarbe2010-08-19
* Fixed a contractGravatar akashlal2010-08-10
* More line ending fixups.Gravatar MichalMoskal2010-08-06
* Boogie: Removed trailing spaces in codeGravatar tabarbe2010-08-04
* Boogie: VCGeneration port part 1/3: Replacing old source files with ported ve...Gravatar tabarbe2010-07-28
* Boogie\VCGeneration: Renaming sources in preparation for my addition of the p...Gravatar tabarbe2010-07-28