Issues
- 3
- 0
Add support for '$' as an identifier character
#74 opened by mww-aws - 1
- 1
Confusions about the verification result
#71 opened by verifierlife - 0
- 0
user specified precision in rational printing
#67 opened by lgwagner - 0
- 3
loop operation in Lustre
#66 opened by verifierlife - 3
Z3 parse error during division
#63 opened by TimArnettThales - 1
SmtLib2 Parser does not work for z3 models
#60 opened by mgudemann - 2
Array assignment
#65 opened by verifierlife - 4
- 1
JKind breaks with condacts in Java 9+
#61 opened by lgwagner - 2
K-induction fails with SMTInterpol Exception
#58 opened by mgudemann - 1
Output parse error when using Z3
#59 opened by mister-walter - 1
Unsound interaction between arrays and subranges
#50 opened by yav - 2
Arithmetic Exception
#47 opened by lgwagner - 4
smtlib2 parse error
#46 opened by TheBeaNerd - 1
Z3-related crash regarding parsing Solver output
#45 opened by lgwagner - 2
Uncaught Exception
#44 opened by lgwagner - 0
PDR soundness bug with assertions
#43 opened by agacek - 1
- 3
Non-constant division
#30 opened by lememta - 4
jKind Starting Script (on a Mac)
#28 opened by AFifarek - 1
Stack Overflow
#27 opened by lgwagner - 0
- 2
Out of memory error on active-standby.kind.lus
#23 opened by mebsout - 7
Jkind 2.1 requires Java 8
#21 opened by lwrage - 2
Z3 may produce invalid counter-examples
#20 opened by Greg4cr - 0
- 7
Support for Casting
#17 opened by Greg4cr - 6
JKind prevents use of non-constant multiplication/division, regardless of solver
#16 opened by Greg4cr - 0
Null Pointer Exceptions
#15 opened by lgwagner - 2
incorrect scripts for Linux
#14 opened by lgwagner - 1
Allow constant expressions in subrange types
#7 opened by agacek - 0
Flag unguarded pre results in counterexamples
#13 opened by agacek - 1
Handle assertions and properties in subnodes
#10 opened by agacek - 1
Additional static checks
#11 opened by agacek - 0
Allow proposed invariants
#12 opened by agacek - 0
Differentiate unknown results
#9 opened by agacek - 1
Report invariants used
#8 opened by agacek - 0
JKind does not detect division by zero
#6 opened by agacek - 0
If an unknown identifier appears in a property, JKind will throw an NPE rather than yielding a descriptive error.
#5 opened by lgwagner - 2
Inductive Counterexample
#2 opened by lgwagner - 1
Verbose output
#3 opened by lgwagner - 0
Bug in inlining
#4 opened by agacek - 2
Yices output parser appears broken...
#1 opened by lgwagner