---
name: "yosys-smtbmc"
section: "1"
platform: "linux"
package: "yosys"
version: "0.52-2"
release: "Debian 13 (Trixie)"
platforms: ["linux"]
url: "https://new.carta.tech/yosys-smtbmc"
---

# yosys-smtbmc(1)

write design to SMT2-LIBv2 file

## NAME

**yosys-smtbmc** - write design to SMT2-LIBv2 file

## SYNOPSIS

```
yosys-smtbmc [options] <yosys_smt2_output>
```

## OPTIONS

- **-t \[\<skip\_steps\>:\]\<num\_steps\>**

  **default: skip\_steps=0, num\_steps=20**

- **-u \<start\_step\>**

  **assume asserts in skipped steps in BMC**

- **-S \<step\_size\>**

  **proof \<step\_size\> time steps at once**

- **-c \<vcd\_filename\>**

  **write counter-example to this VCD file (hint: use 'write\_smt2** **-wires' for maximum coverage of signals in generated VCD file)**

- **-i**

  **instead of BMC run temporal induction**

- **-m \<module\_name\>**

  **name of the top module**

- **-s \<solver\>**

  **Set SMT solver: z3, cvc4, yices, mathsat. default: z3**

- **-v**

  **enable debug output**

- **-p**

  **disable timer display during solving**

- **-d \<filename\>**

  **write smt2 statements to file**

## AUTHOR

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