Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Normalise line endings using a .gitattributes file. Unfortunately | Dan Liew | 2015-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 Ketema | Dan Liew | 2014-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 code | Dan Liew | 2014-09-24 |
| | | | | Patch by Jeroen Ketema | ||
* | Fixed crash in ModelParser when Z3 returns an operator that is a list. | Ken McMillan | 2014-02-21 |
| | |||
* | refactoring | Pantazis Deligiannis | 2013-07-22 |
| | |||
* | refactoring and fixes in the SMTLIB2 parser | Pantazis Deligiannis | 2013-07-19 |
| | |||
* | code cleanup and refactoring | Pantazis Deligiannis | 2013-07-11 |
| | |||
* | code cleanup & refactoring | Pantazis Deligiannis | 2013-07-11 |
| | |||
* | fixed another bug when parsing nested arrays under CVC4 | Pantazis Deligiannis | 2013-07-10 |
| | |||
* | fix a bug when parsing nested arrays under CVC4 | Pantazis Deligiannis | 2013-07-10 |
| | |||
* | the cvc4 parser can now parse nested array expressions | Pantazis Deligiannis | 2013-07-10 |
| | |||
* | added specific command line options to enable the SMTLIB2 output model ↵ | Pantazis Deligiannis | 2013-07-09 |
| | | | | parser for Z3. Use /proverOpt:SMTLIB2_MODEL=true | ||
* | 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 | ||
* | simplified SMTLIB2 parser by merging some parsing methods for the CVC4 and ↵ | pantazis | 2013-06-12 |
| | | | | Z3 sub-parsers | ||
* | fix on parser for bit vectors | pantazis | 2013-06-12 |
| | |||
* | cleaning up some unused code | pantazis | 2013-06-12 |
| | |||
* | Z3 new parser takes now a new option for pp-bv-literals | pantazis | 2013-06-12 |
| | |||
* | CVC4 Parser | pantazis | 2013-06-12 |