Commit message (Collapse) | Author | Age | |
---|---|---|---|
* | Changed the syntax reading of the float type | Checkmate50 | 2016-07-16 |
| | |||
* | fixed some merging issues | Checkmate50 | 2016-06-07 |
| | |||
* | resolving conflicts | Checkmate50 | 2016-06-06 |
|\ | |||
* | | Merging complete. Everything looks good *crosses fingers* | Checkmate50 | 2016-06-06 |
| | | |||
* | | finished testing, fixed several minor compiler bugs | Checkmate50 | 2016-06-06 |
| | | |||
* | | modified floating point syntax and modified floating point constants to use ↵ | Checkmate50 | 2016-03-17 |
| | | | | | | | | bitvector values | ||
| * | Improve support for identifying unnecessary assumes. | Valentin Wüstholz | 2016-03-09 |
| | | |||
| * | Add support for weights on soft assumes. | Valentin Wüstholz | 2016-03-07 |
| | | |||
| * | Improve support for optimization and identifying unnecessary assumes. | Valentin Wüstholz | 2016-03-03 |
| | | |||
* | | Modified BigFloat and parser to accept correct SMT-LIB syntax | Checkmate50 | 2016-02-20 |
| | | |||
| * | Fix issue with ids for assume-statements. | Valentin Wüstholz | 2015-12-28 |
| | | |||
| * | Enable optimization for more prover queries. | Valentin Wüstholz | 2015-12-27 |
| | | |||
* | | Special fp types (such as infinity and NaN are now translated by boogie | Checkmate50 | 2015-11-29 |
| | | |||
| * | Add experimental support for optimization (requires Z3 build after changeset ↵ | Valentin Wüstholz | 2015-11-18 |
| | | | | | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7). | ||
| * | Add support for identifying unnecessary assumes. | Valentin Wüstholz | 2015-11-16 |
| | | |||
* | | Modified translation so that z3 runs with type checking for simple binary ↵ | Checkmate50 | 2015-10-14 |
| | | | | | | | | operations | ||
* | | Modified BigFloat to avoid evaluating the floating point value before ↵ | Checkmate50 | 2015-09-23 |
| | | | | | | | | sending it to z3 | ||
* | | Added initial support for float addition | Checkmate50 | 2015-09-17 |
| | | |||
* | | Float type now works correctly for simple variable declaration and comparison. | Dietrich | 2015-07-20 |
| | | |||
* | | Modified internal abstract float representation to allow user-defined ↵ | Dietrich | 2015-07-13 |
| | | | | | | | | mantissa and exponent | ||
| * | 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. | ||
| * | removed a stray Console.WriteLine that Ken had earlier checked in by | qadeer | 2015-06-25 |
| | | | | | | | | mistake. | ||
| * | Merge branch 'master' of https://github.com/boogie-org/boogie | akashlal | 2015-06-20 |
| |\ | |||
| * | | Fix for reading fixpoint back into boogie exprs | akashlal | 2015-06-20 |
| | | | |||
| | * | adding z3name option | Ken McMillan | 2015-06-15 |
| |/ | |||
| * | Fix minor issue with diagnosing timeouts. | Valentin Wüstholz | 2015-06-12 |
| | | |||
| * | Merge branch 'master' of https://github.com/boogie-org/boogie | Ken McMillan | 2015-06-11 |
| |\ | |||
| | * | fixed crash | qadeer | 2015-06-10 |
| | | | |||
| * | | various changes for duality from dead codeplex repo | U-REDMOND\kenmcmil | 2015-06-09 |
| | | | |||
| | * | Stop truncating the prover logs | Clément Pit--Claudel | 2015-06-09 |
| |/ | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | As it stands, Boogie abruptly aborts the prover by calling Kill() on the associated process after receiving responses to all of its queries. In most cases this is fine, but in general this is pretty bad: it yields to all sorts of output corruption when user-supplied options require z3 to write output to an auxiliary file (say, using /z3opt:TRACE=true). This explains why VCC's Axiom Profiler often complains about a missing [eof] after running Boogie with /z3opt:TRACE=true. This patch fixes it by only falling back to Kill if the process seems to have become unresponsive. That is, it starts by cleanly closing the process input, which signals the end of the interactive session. It then waits for a clean exit for 2s, and only after that does it resort to calling Kill(). I've striven for minimal modifications to the logic, so the patch still universally swallows errors that might occur while closing the underlying stream, and still calls Kill() (I wouldn't be against Boogie just hanging if z3 hangs too). On my tests, z3 exits cleanly pretty much instantly after input is closed anyway, so I don't expect the timeout to fire often (which would be one more reason to actually remove that timeout, and condition Boogie's exit on that of z3 IMO). | ||
| * | Improve support for diagnosing timeouts. | Valentin Wüstholz | 2015-06-08 |
| | | |||
| * | Improve support for diagnosing timeouts. | Valentin Wüstholz | 2015-06-05 |
| | | |||
| * | Improve heuristics for diagnosing timeouts. | Valentin Wüstholz | 2015-05-31 |
| | | |||
| * | Improve support for diagnosing timeouts. | Valentin Wüstholz | 2015-05-22 |
| | | |||
| * | Minor changes | Valentin Wüstholz | 2015-05-20 |
| | | |||
| * | Minor refactoring | Valentin Wüstholz | 2015-05-20 |
| | | |||
| * | Improve support for diagnosing timeouts. | Valentin Wüstholz | 2015-05-20 |
| | | |||
| * | Improve support for diagnosing timeouts. | Valentin Wüstholz | 2015-05-19 |
| | | |||
| * | Add some experimental support for diagnosing timeouts. | Valentin Wüstholz | 2015-05-18 |
| | | |||
| * | Fix for printFixedPoint when dealing with functions | Akash Lal | 2015-05-13 |
| | | |||
* | | integrated the named float type to act as a real in boogie | Dietrich | 2015-05-04 |
| | | |||
* | | Began adding the float type to VC expression | Dietrich | 2015-04-27 |
| | | |||
| * | 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 | ||
* | VC gen for security properties | akashlal | 2015-04-05 |
| | |||
* | If using -proverLog: make sure we flush after writing every line | Dan Liew | 2015-03-10 |
| | | | | | | | | | otherwise if either of the following happens * if the solver hangs and we do CTRL+C * if Boogie crashes then some lines will be missing from the log. | ||
* | Work around bug in Z3 4.3.2 and newer (https://z3.codeplex.com/workitem/188) | Dan Liew | 2015-03-10 |
| | | | | | | where setting produce-unsat-cores to true has no effect unless the option is set last. This makes the Test/houdini/testUnsatCore.bpl test pass under Linux using Z3 4.3.2 | ||
* | Parse Bv values | akashlal | 2015-03-02 |
| | |||
* | 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. |