summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib/SMTLibNamer.cs
Commit message (Expand)AuthorAge
* 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