<commit_before>
# Unreleased

New features:

- New option for checking contracts of imported nodes (see [documentation](https://kind.cs.uiowa.edu/kind2_user_doc/9_other/12_contract_check.html)).
  - Current checks: realizability and satisfiability checking.

Improvements:

- Improve compositional reasoning about assumptions of called nodes.
  - See issue [#736](https://github.com/kind2-mc/kind2/issues/736) for more details (thanks to <NAME>).
- Print values of ghost variables in counterexamples.
- Fix and update bounds checking feature for subrange streams.
  Thanks to <NAME>, <NAME>, and <NAME> for their bug reports.
- Fix issue in MUST set generation when a single MIVC is computed.
- Accept fractions in JSON input for interpreter.
- Other bug fixes.

Changes:

- Always check node calls are safe, not only in compositional mode.
- Set `check_subproperties` flag to true by default.
  - Ignored if modular analysis is true.
- Abstract call only if contract has at least one guarantee or one mode.


# Kind 2 v1.3.1

This release includes performance improvements and various fixes. Notably:

- Fix soundness issue in path compression when there are temporal dependencies
  between input values. (Thank you to <NAME> for finding this bug).
- Fix bug in extraction of an active path during IC3 generalization.
- Improve IC3 performance over large models that contain reals or machine integers.
- Fix issue reading models from the latest version of Z3 (4.8.10).
  It caused a runtime error during IVC generation.

<commit_msg>Fix format for GitHub<commit_after>
# Unreleased

New features:

- New option for checking contracts of imported nodes (see [documentation](https://kind.cs.uiowa.edu/kind2_user_doc/9_other/12_contract_check.html)).
  - Current checks: realizability and satisfiability checking.

Improvements:

- Improve compositional reasoning about assumptions of called nodes.
  - See issue [#736](https://github.com/kind2-mc/kind2/issues/736) for more details (thanks to <NAME>).
- Print values of ghost variables in counterexamples.
- Fix and update bounds checking feature for subrange streams.
  - Thanks to <NAME>, <NAME>, and <NAME> for their bug reports.
- Fix issue in MUST set generation when a single MIVC is computed.
- Accept fractions in JSON input for interpreter.
- Other bug fixes.

Changes:

- Always check node calls are safe, not only in compositional mode.
- Set `check_subproperties` flag to true by default.
  - Ignored if modular analysis is true.
- Abstract call only if contract has at least one guarantee or one mode.


# Kind 2 v1.3.1

This release includes performance improvements and various fixes. Notably:

- Fix soundness issue in path compression when there are temporal dependencies
  between input values.
  - Thank you to <NAME> for finding this bug.
- Fix bug in extraction of an active path during IC3 generalization.
- Improve IC3 performance over large models that contain reals or machine integers.
- Fix issue reading models from the latest version of Z3 (4.8.10).
  It caused a runtime error during IVC generation.


{'fraction_non_alphanumeric': 0.06688311688311688, 'fraction_numerical': 0.014935064935064935, 'mean_word_length': 4.034313725490196, 'pattern_counts': {'":': 0, '<': 13, '<?xml version=': 0, '>': 13, 'https://': 4, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3765609', 'n_tokens_mistral': 848, 'n_tokens_neox': 799, 'n_words': 403}