.\" Text automatically generated by txt2man
.TH YOSYS-SMTBMC 1 "02 November 2018" "" ""
.SH NAME
\fByosys-smtbmc \fP- write design to SMT2-LIBv2 file
\fB
.SH SYNOPSIS
.nf
.fam C
\fByosys-smtbmc\fP [\fIoptions\fP] <yosys_smt2_output>

.fam T
.fi
.fam T
.fi
.SH OPTIONS

.TP
.B
\fB-t\fP [<skip_steps>:]<num_steps>
default: skip_steps=0, num_steps=20
.TP
.B
\fB-u\fP <start_step>
assume asserts in skipped steps in BMC
.TP
.B
\fB-S\fP <step_size>
proof <step_size> time steps at once
.TP
.B
\fB-c\fP <vcd_filename>
write counter-example to this VCD file (hint: use 'write_smt2
\fB-wires\fP' for maximum coverage of signals in generated VCD file)
.TP
.B
\fB-i\fP
instead of BMC run temporal induction
.TP
.B
\fB-m\fP <module_name>
name of the top module
.TP
.B
\fB-s\fP <solver>
Set SMT solver: z3, cvc4, yices, mathsat. default: z3
.TP
.B
\fB-v\fP
enable debug output
.TP
.B
\fB-p\fP
disable timer display during solving
.TP
.B
\fB-d\fP <filename>
write smt2 statements to file
.RE
.PP

.SH AUTHOR

This manual page was written by Sebastian Kuzminsky <seb@highlab.com>
for the Debian project (and may be used by others).