From 3eaaa54afe286269fbcd05de24635981f2633613 Mon Sep 17 00:00:00 2001 From: Thomas Tuegel Date: Thu, 9 Jul 2020 09:21:00 -0500 Subject: [PATCH] kore-0.25.0.0 (#1964) --- kore/CHANGELOG.md | 22 ++++++++++++++++++++++ kore/package.yaml | 2 +- 2 files changed, 23 insertions(+), 1 deletion(-) diff --git a/kore/CHANGELOG.md b/kore/CHANGELOG.md index d6669d5ba8..b89ec48a83 100644 --- a/kore/CHANGELOG.md +++ b/kore/CHANGELOG.md @@ -14,8 +14,30 @@ All notable changes to this project will be documented in this file. ### Fixed +## [0.25.0.0] - 2020-07-08 + +### Added + +- The `simplification` attribute takes an optional integer argument indicating + the priority of the simplification rule. +- The hooked function `INT.ediv` implements Euclidean division. + +### Changed + +- `ErrorBottomTotalFunction` is thrown when a function declared total + (`functional`) returns `\bottom`. +- `ErrorDecidePredicateUnknown` is thrown when the solver cannot decide if a + condition is satisfiable or unsatisfiable. + +### Fixed + - `kore-exec` exits with the code specified by the semantics, even when the final configuration has side conditions. +- `kore-exec` and `kore-repl` halt when the limit specified by the `--breadth` + option is exceeded. +- Proofs are no longer incomplete when the final configuration is undefined. +- `kore-repl` does not allow `clear`-ing the direct child of a branching node + because this can invalidate a proof. ## [0.24.0.0] - 2020-06-25 diff --git a/kore/package.yaml b/kore/package.yaml index 9d91dc9221..a405577b38 100644 --- a/kore/package.yaml +++ b/kore/package.yaml @@ -1,5 +1,5 @@ name: kore -version: 0.24.0.0 +version: 0.25.0.0 github: "kframework/kore" license: NCSA license-file: LICENSE