KIND-INV -- Inductive invariant generator for Lustre programs

Usage: kind-inv [-inv_int and/or -inv_bool][options] input_file

Options:

  -node 	:User specified main node (default: the last node that contains a PROPERTY)

  -inv_bool 	:Generate boolean implication type invariants

  -inv_int 	:Generate integer less_or_equal type invariants

  -rm_trivial_inv :Leave trivial invariants there (default: Remove trivial invariants)

  -range :Maximum range for which to generate candidates for mode variables (default: max range = 10)

  -yices_exec 	:Use Yices executable as solver (default: yices)

  -debug 	:Include debugging output (default: false)

  -quiet 	:Only return final answer (default: true)

  -verbose 	:Return more details (default: false)

  -version :Print version & copyright information

  -help  :Display this list of options

  --help  :Display this list of options
