From: Clifford Wolf Date: Sun, 22 Feb 2015 15:30:02 +0000 (+0100) Subject: Minor "write_smt2" help msg change X-Git-Tag: yosys-0.6~392 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ff3f2448b18ce01a7af876816df8f03cf32f3145;p=yosys.git Minor "write_smt2" help msg change --- diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 50cb74ad8..1525d32ff 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -622,7 +622,7 @@ struct Smt2Backend : public Backend { log("The following yosys script will create a 'test.smt2' file for our proof:\n"); log("\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("\n"); log("Running 'cvc4 test.smt2' will print 'unsat' because y can never transition\n");