riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

fix typo in `write_smt2` help

This commit is contained in:
Teguh Hofstee 2020-03-23 02:14:26 -07:00
parent c34969d3f1
commit b08932cb81
2 changed files with 2 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
backends/smt2/smt2.cc
View File

@ -1394,7 +1394,7 @@ struct Smt2Backend : public Backend {
log("\n"); log("\n");
log("For this proof we create the following template (test.tpl).\n"); log("For this proof we create the following template (test.tpl).\n");
log("\n"); log("\n");
log(" ; we need QF_UFBV for this poof\n"); log(" ; we need QF_UFBV for this proof\n");
log(" (set-logic QF_UFBV)\n"); log(" (set-logic QF_UFBV)\n");
log("\n"); log("\n");
log(" ; insert the auto-generated code here\n"); log(" ; insert the auto-generated code here\n");

2
manual/command-reference-manual.tex
View File

@ -5350,7 +5350,7 @@ never transition from a non-zero value to a zero value.
For this proof we create the following template (test.tpl). For this proof we create the following template (test.tpl).
; we need QF_UFBV for this poof ; we need QF_UFBV for this proof
(set-logic QF_UFBV) (set-logic QF_UFBV)
; insert the auto-generated code here ; insert the auto-generated code here