<commit_before>JKind
=====

JKind is a Java implementation of the [Kind 2 model
checker](http://kind2-mc.github.io/kind2/). Kind 2 is a multi-engine
SMT-based automatic model checker for safety properties of Lustre
programs.

Downloads
---------

The latest release of JKind is available on the [releases
page](https://github.com/agacek/jkind/releases). This includes the
JKind model checker as well as the Lustre2excel and Lustre2kind
utilities.

Design Goals
------------

JKind is designed to be cross-platform, reliable, and easy to extend.
Power and performance are secondary goals. Additionally, JKind
attempts to be mostly compatible with pkind and Kind 2, though this
varies over time due to developments in both systems.


Installation Notes
------------------

By default, JKind requires [Yices (version
1)](http://yices.csl.sri.com/download-yices1.shtml) to be installed on
your PATH. Alternatively, one can use
[CVC4](http://cvc4.cs.nyu.edu/web/), [Z3](https://github.com/Z3Prover/z3),
[Yices 2](http://yices.csl.sri.com/index.shtml),
[MathSAT](http://mathsat.fbk.eu/), or
[SMTInterpol](http://ultimate.informatik.uni-freiburg.de/smtinterpol/).<commit_msg>Update README.md to reflect build-in SMTInterpol<commit_after>JKind
=====

JKind is a Java implementation of the [Kind 2 model
checker](http://kind2-mc.github.io/kind2/). Kind 2 is a multi-engine
SMT-based automatic model checker for safety properties of Lustre
programs.

Downloads
---------

The latest release of JKind is available on the [releases
page](https://github.com/agacek/jkind/releases). This includes the
JKind model checker as well as the Lustre2excel and Lustre2kind
utilities.

Design Goals
------------

JKind is designed to be cross-platform, reliable, and easy to extend.
Power and performance are secondary goals. Additionally, JKind
attempts to be mostly compatible with pkind and Kind 2, though this
varies over time due to developments in both systems.


Alternative Solvers (optional)
------------------------------

By default, JKind is packaged with [SMTInterpol](http://ultimate.informatik.uni-freiburg.de/smtinterpol/) 
as its underlying SMT solver. Advanced users may wish to install alternative solvers such as 
[Z3](https://github.com/Z3Prover/z3),
[Yices (version 1)](http://yices.csl.sri.com/download-yices1.shtml) 
[Yices 2](http://yices.csl.sri.com/index.shtml),
[CVC4](http://cvc4.cs.nyu.edu/web/), or
[MathSAT](http://mathsat.fbk.eu/).
{'fraction_non_alphanumeric': 0.14010651372388366, 'fraction_numerical': 0.012290045063498567, 'mean_word_length': 3.8548707753479126, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 3, 'https://': 4, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 4, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '6550508', 'n_tokens_mistral': 808, 'n_tokens_neox': 777, 'n_words': 254}