diff options
| author | Clifford Wolf <clifford@clifford.at> | 2016-09-18 20:48:09 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2016-09-18 20:48:09 +0200 |
| commit | d009cdd6eef5a24a11584a543bab8543f3940f6c (patch) | |
| tree | 5601d0ddb658f0239c15bb3722bff4f3e868115a /backends/smt2/smt2.cc | |
| parent | 13a03b84d402d4a9891e6513a44551572d3e92db (diff) | |
| download | yosys-d009cdd6eef5a24a11584a543bab8543f3940f6c.tar.gz yosys-d009cdd6eef5a24a11584a543bab8543f3940f6c.tar.bz2 yosys-d009cdd6eef5a24a11584a543bab8543f3940f6c.zip | |
Improved handling of SMT2 logics in yosys-smtbmc
Diffstat (limited to 'backends/smt2/smt2.cc')
| -rw-r--r-- | backends/smt2/smt2.cc | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index e07515133..9a25f3a23 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -998,7 +998,7 @@ struct Smt2Backend : public Backend { continue; } if (args[argidx] == "-nomem") { - bvmode = false; + memmode = false; continue; } if (args[argidx] == "-wires") { @@ -1027,6 +1027,12 @@ struct Smt2Backend : public Backend { *f << stringf("; SMT-LIBv2 description generated by %s\n", yosys_version_str); + if (!bvmode) + *f << stringf("; yosys-smt2-nobv\n"); + + if (!memmode) + *f << stringf("; yosys-smt2-nomem\n"); + std::vector<RTLIL::Module*> sorted_modules; // extract module dependencies |