summaryrefslogtreecommitdiff
path: root/Source/Model
Commit message (Collapse)AuthorAge
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-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.
* Patch by Jeroen KetemaGravatar Dan Liew2014-12-01
| | | | | | | | | | Fix some of the interfacing with Z3 4.3.2 in SMTLib. In particular: * It makes the useSmtOutputFormat usable * It fixes parsing of bit vectors that occur in the models returned by Z3 Similar stuff might be broken in the other interfaces to Z3, but it shouldn’t be more broken than it already was.
* Remove dead method argumentGravatar Dan Liew2014-09-24
| | | | Patch by Jeroen Ketema
* Remove dead codeGravatar Dan Liew2014-09-24
| | | | Patch by Jeroen Ketema
* Fixed crash in ModelParser when Z3 returns an operator that is a list.Gravatar Ken McMillan2014-02-21
|
* Fix Boogie so it compiled with mono. Patch by Dan Liew.Gravatar Ally Donaldson2014-01-14
|
* added the QED build configurationGravatar qadeer2013-12-02
|
* Fixed several build errors in the 'Checked' configuration.Gravatar wuestholz2013-08-05
|
* Whitespace fixGravatar Ally Donaldson2013-07-22
|
* refactoringGravatar Pantazis Deligiannis2013-07-22
|
* refactoring and fixes in the SMTLIB2 parserGravatar Pantazis Deligiannis2013-07-19
|
* code cleanup and refactoringGravatar Pantazis Deligiannis2013-07-11
|
* code cleanup & refactoringGravatar Pantazis Deligiannis2013-07-11
|
* fixed another bug when parsing nested arrays under CVC4Gravatar Pantazis Deligiannis2013-07-10
|
* fix a bug when parsing nested arrays under CVC4Gravatar Pantazis Deligiannis2013-07-10
|
* the cvc4 parser can now parse nested array expressionsGravatar Pantazis Deligiannis2013-07-10
|
* added specific command line options to enable the SMTLIB2 output model ↵Gravatar Pantazis Deligiannis2013-07-09
| | | | parser for Z3. Use /proverOpt:SMTLIB2_MODEL=true
* fixed the CVC4 SMTLIB array parsing to work under the latest CVC4 model ↵Gravatar pantazis2013-06-13
| | | | representation changes
* merged more CVC4 and Z3 SMTLIB2 parsing methods ... results into a more ↵Gravatar pantazis2013-06-13
| | | | compact parser
* simplified SMTLIB2 parser by merging some parsing methods for the CVC4 and ↵Gravatar pantazis2013-06-12
| | | | Z3 sub-parsers
* fix on parser for bit vectorsGravatar pantazis2013-06-12
|
* cleaning up some unused codeGravatar pantazis2013-06-12
|
* Z3 new parser takes now a new option for pp-bv-literalsGravatar pantazis2013-06-12
|
* small update in optionsGravatar pantazis2013-06-12
|
* naive SMTLIB2 ParserGravatar pantazis2013-06-12
|
* CVC4 ParserGravatar pantazis2013-06-12
|
* fixed bug in model printingGravatar Unknown2013-03-11
| | | | reverted a previous erroneous fix I had made in model parsing
* updated the model parsing (probably caused by some change in Z3's output)Gravatar Unknown2013-03-07
|
* bug fix in model printingGravatar Unknown2013-01-04
|
* Model: sort variables by nameGravatar Peter Collingbourne2012-06-26
| | | | This makes the model file much easier to read.
* Dafny/Boogie/BVD: made Dafny plug-in for BVD work againGravatar Rustan Leino2012-06-08
|
* fixed a problem in model parsingGravatar Unknown2012-02-08
| | | | (_ BitVec n) is substituted with bvn
* fixed bug in model parsingGravatar qadeer2012-02-06
| | | | converted a bunch of definitions to be inlined
* a bug fix in model parsingGravatar qadeer2011-11-30
|
* fixed a bug in model parsingGravatar qadeer2011-11-28
|
* fixed another bug in model parser related to datatype valuesGravatar qadeer2011-11-14
| | | | cleaned up the code related to v1model
* some refactoring suggested by MichalGravatar qadeer2011-11-07
|
* change in model parsing with datatype valuesGravatar qadeer2011-11-07
|
* Performance improvements in BVDGravatar Michal Moskal2011-10-19
|
* Added some extra functionality to Model code for corralGravatar Unknown2011-09-13
|
* Another test checkinGravatar Michal Moskal2011-07-12
|
* ported all the counterexample code to Michal's new Model class; the goal is ↵Gravatar Unknown2011-06-27
| | | | to eliminate the class ErrorModel from the codebase.
* Dafny: compile quantifiersGravatar rustanleino2011-03-26
| | | | | | Dafny: allow {:induction} attribute to take an explicit list of bound variables on which to apply induction Dafny: split expressions when proving function postconditions Boogie and BVD: updated copyright year ranges
* Re-enabled quantifier checking in the Checked configuration.Gravatar mikebarnett2011-03-16
|
* Turn off quantifier checking in the runtime checking.Gravatar mikebarnett2011-03-14
|
* Added a new solution configuration, Checked, that builds the Checked ↵Gravatar mikebarnett2011-03-07
| | | | configuration of each project. Turned on runtime checking and reference assembly generation for all of the projects, but only in the Checked configuration.
* Handle as-array[...] model elementsGravatar MichalMoskal2011-02-23
|
* Parse else-> clauses in the modelGravatar MichalMoskal2011-02-23
| | | | Disable MODEL_PARTIAL in SMTLib
* Set Id of Elements.Gravatar MichalMoskal2011-02-21
| | | | Add some explanation at the beginning of the file.
* Accomodate for recent changes in Z3 V2 model formatGravatar MichalMoskal2011-02-18
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-18 15:50:07 +0000