Skip to content

JKind v1.6
Compare
Choose a tag to compare
@agacek agacek released this 04 Sep 13:16
· 378 commits to master since this release
v1.6
589a09e

Features

  • New backend SMT translation avoids uninterpreted functions. In general, this means much better performance for larger/harder models.
  • Support for Yices 2 (using yices-smt2 executable).
  • Support for Kind 2 (local and remote) in JKind API.
  • Improved invariant generation for integers with fixed initial values.
  • Support for JKIND_HOME, YICES_HOME, YICES2_HOME, Z3_HOME, and CVC4_HOME environment variables for users who do not want to put JKind or their SMT solvers in their PATH.
  • New NodeBuilder and ProgramBuilder objects in JKind API to make it easier to construct nodes and programs in an imperative style.

Fixes

  • Fix bug in model evaluation related to subtraction
  • Improved error messages for bad file name inputs
Assets 3
Loading