diff options
| author | Clifford Wolf <clifford@clifford.at> | 2016-08-17 20:10:02 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2016-08-17 20:10:02 +0200 |
| commit | dfcd30ea869f43af520aef033aa1311457112904 (patch) | |
| tree | 6d066b6dc33fbc15499333c281becea6bc6d9cea /backends/smt2/smt2.cc | |
| parent | 42a971226bd1972c3c21d386c02c1bc2ac850129 (diff) | |
| download | yosys-dfcd30ea869f43af520aef033aa1311457112904.tar.gz yosys-dfcd30ea869f43af520aef033aa1311457112904.tar.bz2 yosys-dfcd30ea869f43af520aef033aa1311457112904.zip | |
Added printing of code loc of failed asserts to yosys-smtbmc
Diffstat (limited to 'backends/smt2/smt2.cc')
| -rw-r--r-- | backends/smt2/smt2.cc | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 584a1df1a..da65b7bce 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -605,8 +605,10 @@ struct Smt2Worker if (cell->type.in("$assert", "$assume")) { string name_a = get_bool(cell->getPort("\\A")); string name_en = get_bool(cell->getPort("\\EN")); + decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, log_id(module), idcounter, + cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : log_id(cell))); decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n", - log_id(module), idcounter, log_id(module), name_a.c_str(), name_en.c_str(), log_id(cell))); + log_id(module), idcounter, log_id(module), name_a.c_str(), name_en.c_str(), log_id(cell))); if (cell->type == "$assert") assert_list.push_back(stringf("(|%s#%d| state)", log_id(module), idcounter++)); else |