Issues
- 0
Top-level array definition causes runtime failures
#1043 opened by amosr - 0
Realizability check terminates unexpectedly when computing deadlocking trace
#1036 opened by andreaskatis - 3
- 2
Problem with simulation both in VSCode and in the web app
#1007 opened by ploc - 1
Error with multidimensional array constructor
#951 opened by kumori123 - 1
- 1
- 5
- 2
Exit code 20 on a seemingly successful analysis
#917 opened by erooke - 1
- 2
a problem on Lustre grammar supported by Kind2
#916 opened by kumori123 - 0
Could kind2 run on windows without WSL?
#932 opened by kumori123 - 0
Support automaton
#919 opened by kumori123 - 2
problem: cannot find z3
#915 opened by kumori123 - 1
Contract Ghost variables
#573 opened by hbourbouh - 14
- 0
- 1
- 1
Solver error invoking node with quantified variable
#673 opened by xaaronc - 0
Problem type checking array sizes in node instances
#566 opened by tbrk - 0
- 1
Nodes declaration order in Contracts
#538 opened by hbourbouh - 2
- 2
Compilation error with `4.05.0`
#639 opened by mgudemann - 5
- 2
Property / test coverage (feature request)
#744 opened by amosr - 3
Soundness bug with subrange types
#721 opened by xaaronc - 5
- 1
Type error with subrange int in arrays
#707 opened by Vivi-yd - 0
- 1
Unary negation on subrange type unsat initial state
#670 opened by xaaronc - 5
Abstract analysis of assume-only contracts
#645 opened by xaaronc - 1
Duplicated properties fail with slice_nodes disabled
#643 opened by amosr - 2
- 2
What Cannot generalize quantified terms means?
#634 opened by hbourbouh - 2
Verification of liveness properties
#633 opened by SweeWarman - 2
- 1
Compilation fails on 4.07.0
#616 opened by 5nizza - 2
- 1
top-down analysis of each node
#601 opened by hbourbouh - 5
Failure to run ./build.sh
#598 opened by mfry90 - 1
Imported node sometimes prevents refinement
#596 opened by xaaronc - 2
Asserts in sub-nodes do not produce proof obligations
#595 opened by amosr - 1
Kind2 fails to build
#562 opened by hbourbouh - 2
interpreter fails with automaton
#561 opened by hbourbouh - 2
BMC Unrolling of the system is unsat at 1, the system has no more reachable states.
#560 opened by anmavrid - 7
Runtime error in invariant manager
#558 opened by hbourbouh - 1
timeout_analysis
#557 opened by hbourbouh - 1
Can kind2 check this kind of code?
#517 opened by stanislaw - 0
Simplification of to-real
#504 opened by correnson