| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Add experimental support for optimization (requires Z3 build after changeset ↵ |  Valentin Wüstholz | 2015-11-18 |
| | | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). | ||
| * | 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. | ||
| * | Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has a | Dan Liew | 2015-04-26 |
| | | | | | | variable that begins with a ``.``. This was't an issue for Z3 which ignores this but CVC4 is stricter and will emit an error | ||
| * | Fix using "mkbv" as a variable name in a boogie program. This was | Dan Liew | 2015-02-27 |
| | | | | | | taken from ``bv_decl_plugin::get_op_names(...)`` in ``src/ast/bv_decl_plugin.cpp`` in the Z3 4.3.2 source code. | ||
| * | Fix using reserved Z3 keywords for real/int arithmetic operators. These are ↵ | Dan Liew | 2015-02-27 |
| | | | | | | | | taken from `` arith_decl_plugin::get_op_names(...)`` from ``src/ast/arith_decl_plugin.cpp`` in the Z3 4.3.2 source code. | ||
| * | Fix using reserved Z3 keywords for float operators. These are taken | Dan Liew | 2015-02-27 |
| | | | | | | from ``float_decl_plugin::get_op_names(..)`` in ``src/ast/float_decl_plugin.cpp`` from the Z3 4.3.2 source code. | ||
| * | Fix bug where some reserved Z3 keywords were not sanitized | Dan Liew | 2015-02-18 |
| | | | | | when generating the VC. | ||
| * | Boogie: added type 'real' with overloaded arithmetic operations plus real ↵ |  boehmes | 2012-09-27 |
| | | | | | | | | | | division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real'; Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted; Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs); Extended the BigDec class with additional functionality; Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested) | ||
| * | added floating point keywords to reserved SMTwords list |  qadeer | 2012-02-20 |
| | | |||
| * | SMTLib: Only use (set-logic ...) when requested; quote some more symbols |  Michal Moskal | 2011-06-30 |
| | | |||
| * | Replaced all dictionaries that mapped to bool (i.e., were being used to ↵ | mikebarnett | 2011-03-10 |
| | | | | | implement a set) with HashSet. Added a new NonNull method to the cce class that checks to make sure a set is non-null and does not contain null. | ||
| * | Add MULTI_TRACES prover option (equivalent of /z3multipleErrors) | MichalMoskal | 2011-02-23 |
| | | |||
| * | Remove workaround for Z3 scanner problems (fixed now); fix one comment | MichalMoskal | 2011-02-18 |
| | | |||
| * | Handle bitvectors | MichalMoskal | 2011-02-18 |
| | | |||
| * | Use explicit mechanism for skipping to the next assertion | MichalMoskal | 2011-02-17 |
| | | |||
| * | Fix printing of type-proxies | MichalMoskal | 2011-02-16 |
| | | |||
| * | Workaround bug in Z3 SMT parser | MichalMoskal | 2011-02-15 |
| | | |||
| * | Use SMT2 top-level syntax | MichalMoskal | 2011-02-15 |
| | | |||
| * | Print terms in SMT2 syntax (drop term/formula distinction) | MichalMoskal | 2011-02-15 |
| | | |||
| * | Move name-quoting (already for SMT2 not SMT1) into a seprate class | MichalMoskal | 2011-02-15 |
 |
index : debian-boogie | |
| Debian packaging for Boogie |
| summaryrefslogtreecommitdiff |