Skip to content

JKind v1.4.3
Compare
Choose a tag to compare
@agacek agacek released this 18 Oct 18:26
· 515 commits to master since this release
v1.4.3
612656c

Major Features

  • Support for interval generalization of counterexamples via the -interval command line flag. This is based on work by John Backes.
  • Support for condact expressions.

Minor Features

  • Now generates invariant candidates of the form 'x >= 0' for non-combinatorial variables x. This should cover many common invariants when using counters and timers.
  • Improved the layout of counterexamples in the console output.
  • Disabled integer division by negative numbers due to inconsistent interpretations between solvers.
  • Allow -no_inv_gen and -reduce_inv flag together since even without automatic invariant generation, properties may be used as invariants to each other and thus invariant reduction still makes sense.
Assets 3
Loading