summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib
Commit message (Expand)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 b...Gravatar Checkmate502016-03-17
| * 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
| * Add support for identifying unnecessary assumes.Gravatar Valentin Wüstholz2015-11-16
* | Modified translation so that z3 runs with type checking for simple binary ope...Gravatar Checkmate502015-10-14
* | Modified BigFloat to avoid evaluating the floating point value before sending...Gravatar Checkmate502015-09-23
* | 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 mantiss...Gravatar Dietrich2015-07-13
| * Normalise line endings using a .gitattributes file. UnfortunatelyGravatar Dan Liew2015-06-28
| * removed a stray Console.WriteLine that Ken had earlier checked in byGravatar qadeer2015-06-25
| * 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
| |/
| * 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
|/
* VC gen for security propertiesGravatar akashlal2015-04-05
* If using -proverLog: make sure we flush after writing every lineGravatar Dan Liew2015-03-10
* Work around bug in Z3 4.3.2 and newer (https://z3.codeplex.com/workitem/188)Gravatar Dan Liew2015-03-10
* Parse Bv valuesGravatar akashlal2015-03-02
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 20:40:35 +0000