summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/SMTLibNamer.cs
Commit message (Expand)AuthorAge
* Add experimental support for optimization (requires Z3 build after changeset ...Gravatar Valentin Wüstholz2015-11-18
* Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
* Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has aGravatar Dan Liew2015-04-26
* Fix using "mkbv" as a variable name in a boogie program. This wasGravatar Dan Liew2015-02-27
* Fix using reserved Z3 keywords for real/int arithmetic operators. These are t...Gravatar Dan Liew2015-02-27
* Fix using reserved Z3 keywords for float operators. These are takenGravatar Dan Liew2015-02-27
* Fix bug where some reserved Z3 keywords were not sanitizedGravatar Dan Liew2015-02-18
* Boogie: added type 'real' with overloaded arithmetic operations plus real div...Gravatar boehmes2012-09-27
* added floating point keywords to reserved SMTwords listGravatar qadeer2012-02-20
* SMTLib: Only use (set-logic ...) when requested; quote some more symbolsGravatar Michal Moskal2011-06-30
* Replaced all dictionaries that mapped to bool (i.e., were being used to imple...Gravatar mikebarnett2011-03-10
* Add MULTI_TRACES prover option (equivalent of /z3multipleErrors)Gravatar MichalMoskal2011-02-23
* Remove workaround for Z3 scanner problems (fixed now); fix one commentGravatar MichalMoskal2011-02-18
* Handle bitvectorsGravatar MichalMoskal2011-02-18
* Use explicit mechanism for skipping to the next assertionGravatar MichalMoskal2011-02-17
* Fix printing of type-proxiesGravatar MichalMoskal2011-02-16
* Workaround bug in Z3 SMT parserGravatar MichalMoskal2011-02-15
* Use SMT2 top-level syntaxGravatar MichalMoskal2011-02-15
* Print terms in SMT2 syntax (drop term/formula distinction)Gravatar MichalMoskal2011-02-15
* Move name-quoting (already for SMT2 not SMT1) into a seprate classGravatar MichalMoskal2011-02-15
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 04:12:17 +0000