EBMC

Command-line Options

Additional options
--bound nr set bound (default: 1)
--module module set module (default: main)
--property expr specify a property
--outfile name set output file name (default: stdout)
--vcd vcd filename generate traces in VCD format
--show-claims list the properties
--claim nr check a specific property
-I path set include path
 
Methods:
--k-induction do k-induction with k=bound
--interpolation use bit-level interpolants
--interpolation-word use word-level interpolants
--diameter perform recurrence diameter test
 
Solvers:
--dimacs output CNF in Dimacs CNF format
--smt output word-level in SMT format
--smt2 output word-level in SMT 2 format
--boolector use Boolector as solver
--cvc3 use CVC3 as solver
--yices use Yices as solver
--z3 use Z3 as solver
 
Debugging options:
--no-netlist do not generate netlist
--show-parse show parse trees
--show-varmap show variable map
--show-netlist show netlist
--show-ldg show latch dependencies
--smv-netlist show netlist in SMV format
--dot-netlist show netlist in DOT format