mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-11-04 05:19:11 +00:00
Code Activity

Minor "write_smt2" help msg change

Browse source
This commit is contained in:
Clifford Wolf 2015-02-22 16:30:02 +01:00
parent c4f383e452
commit ff3f2448b1
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
backends/smt2/smt2.cc
View file

@ -622,7 +622,7 @@ struct Smt2Backend : public Backend {
log("The following yosys script will create a 'test.smt2' file for our proof:\n"); log("The following yosys script will create a 'test.smt2' file for our proof:\n");
log("\n"); log("\n");
log(" read_verilog test.v\n"); log(" read_verilog test.v\n");
log(" hierarchy; proc; techmap; opt -fast\n"); log(" hierarchy -check; proc; opt; check -assert\n");
log(" write_smt2 -bv -tpl test.tpl test.smt2\n"); log(" write_smt2 -bv -tpl test.tpl test.smt2\n");
log("\n"); log("\n");
log("Running 'cvc4 test.smt2' will print 'unsat' because y can never transition\n"); log("Running 'cvc4 test.smt2' will print 'unsat' because y can never transition\n");