summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib
Commit message (Collapse)AuthorAge
* Changed the syntax reading of the float typeGravatar Checkmate502016-07-16
|
* fixed some merging issuesGravatar Checkmate502016-06-07
|
* resolving conflictsGravatar Checkmate502016-06-06
|\
* | Merging complete. Everything looks good *crosses fingers*Gravatar Checkmate502016-06-06
| |
* | finished testing, fixed several minor compiler bugsGravatar Checkmate502016-06-06
| |
* | modified floating point syntax and modified floating point constants to use ↵Gravatar Checkmate502016-03-17
| | | | | | | | bitvector values
| * Improve support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2016-03-09
| |
| * Add support for weights on soft assumes.Gravatar Valentin Wüstholz2016-03-07
| |
| * Improve support for optimization and identifying unnecessary assumes.Gravatar Valentin Wüstholz2016-03-03
| |
* | Modified BigFloat and parser to accept correct SMT-LIB syntaxGravatar Checkmate502016-02-20
| |
| * Fix issue with ids for assume-statements.Gravatar Valentin Wüstholz2015-12-28
| |
| * Enable optimization for more prover queries.Gravatar Valentin Wüstholz2015-12-27
| |
* | Special fp types (such as infinity and NaN are now translated by boogieGravatar Checkmate502015-11-29
| |
| * Add experimental support for optimization (requires Z3 build after changeset ↵Gravatar Valentin Wüstholz2015-11-18
| | | | | | | | 9cba63c31f6f1466dd4ef442bb840d1ab84539c7).
| * Add support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2015-11-16
| |
* | Modified translation so that z3 runs with type checking for simple binary ↵Gravatar Checkmate502015-10-14
| | | | | | | | operations
* | Modified BigFloat to avoid evaluating the floating point value before ↵Gravatar Checkmate502015-09-23
| | | | | | | | sending it to z3
* | Added initial support for float additionGravatar Checkmate502015-09-17
| |
* | Float type now works correctly for simple variable declaration and comparison.Gravatar Dietrich2015-07-20
| |
* | Modified internal abstract float representation to allow user-defined ↵Gravatar Dietrich2015-07-13
| | | | | | | | mantissa and exponent
| * Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-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 byGravatar qadeer2015-06-25
| | | | | | | | mistake.
| * Merge branch 'master' of https://github.com/boogie-org/boogieGravatar akashlal2015-06-20
| |\
| * | Fix for reading fixpoint back into boogie exprsGravatar akashlal2015-06-20
| | |
| | * adding z3name optionGravatar Ken McMillan2015-06-15
| |/
| * Fix minor issue with diagnosing timeouts.Gravatar Valentin Wüstholz2015-06-12
| |
| * Merge branch 'master' of https://github.com/boogie-org/boogieGravatar Ken McMillan2015-06-11
| |\
| | * fixed crashGravatar qadeer2015-06-10
| | |
| * | various changes for duality from dead codeplex repoGravatar U-REDMOND\kenmcmil2015-06-09
| | |
| | * Stop truncating the prover logsGravatar Clément Pit--Claudel2015-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.Gravatar Valentin Wüstholz2015-06-08
| |
| * Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-06-05
| |
| * Improve heuristics for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-31
| |
| * Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-22
| |
| * Minor changesGravatar Valentin Wüstholz2015-05-20
| |
| * Minor refactoringGravatar Valentin Wüstholz2015-05-20
| |
| * Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-20
| |
| * Improve support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-19
| |
| * Add some experimental support for diagnosing timeouts.Gravatar Valentin Wüstholz2015-05-18
| |
| * Fix for printFixedPoint when dealing with functionsGravatar Akash Lal2015-05-13
| |
* | integrated the named float type to act as a real in boogieGravatar Dietrich2015-05-04
| |
* | Began adding the float type to VC expressionGravatar Dietrich2015-04-27
| |
| * Try to fix the emission of invalid SMT-LIBv2 queries when Boogie has aGravatar Dan Liew2015-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 propertiesGravatar akashlal2015-04-05
|
* If using -proverLog: make sure we flush after writing every lineGravatar Dan Liew2015-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)Gravatar Dan Liew2015-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 valuesGravatar akashlal2015-03-02
|
* Fix using "mkbv" as a variable name in a boogie program. This wasGravatar Dan Liew2015-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 ↵Gravatar Dan Liew2015-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 takenGravatar Dan Liew2015-02-27
| | | | | from ``float_decl_plugin::get_op_names(..)`` in ``src/ast/float_decl_plugin.cpp`` from the Z3 4.3.2 source code.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 17:38:47 +0000