From 46908bfa37a6dcad81644fd3092669891dbf2e50 Mon Sep 17 00:00:00 2001 From: Daniel Larraz Date: Wed, 22 May 2024 14:44:11 -0500 Subject: [PATCH] Update CHANGES.md --- CHANGES.md | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index 189cc2a2f..e751a850f 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -8,16 +8,16 @@ New features: - A new type constructor, [history](https://kind.cs.uiowa.edu/kind2_user_doc/2_input/6_history_type.html), to refer to an unbounded number of previous values of a stream Improvements: -- Optimize encoding of counters in reachability queries -- Apply slicing per IC3IA engine instance -- Fix issue where checks on assumptions of called nodes were not instantiated if an intermediate node has no properties +- Optimized encoding of counters in reachability queries +- Fixed issue where checks on assumptions of called nodes were not instantiated if an intermediate node has no properties +- The new version applies slicing per IC3IA engine instance Changes: -- For imported nodes and functions, Kind 2 now makes the conservative assumption that each output stream is dependent on the current values of all the inputs. The user must refine the model to rule out false positives of circular dependencies -- A call to a node without contract but with at least one output that has a subrange type is now abstracted. Subrange types are now a special case of refinement types, which are handled as an extension of the contract's node, or as the only specification if none is provided -- Undefined initial values and values of undefined output streams with a subrange type range over the base integer type. +- For imported nodes and functions, Kind 2 now assumes conservatively that each output stream depends on the current values of all inputs. The user must refine the model to avoid false positives of circular dependencies +- A call to a node without a contract but with at least one output that has a subrange type is now abstracted. Subrange types are now treated as a special case of refinement types, handled as an extension of the contract's node, or as the sole specification if none is provided +- Undefined initial values and values of undefined output streams with a subrange type range over the base integer type - The type of constants must be provided in their declaration -- Now invariant generation engines always start generating invariants from the top +- Invariant generation engines now always start generating invariants from the top # Kind 2 v2.1.1