diff options
| author | Ahmed Irfan <ahmedirfan1983@gmail.com> | 2014-01-25 19:33:24 +0100 |
|---|---|---|
| committer | Ahmed Irfan <ahmedirfan1983@gmail.com> | 2014-01-25 19:33:24 +0100 |
| commit | 0325efe17214974866be18839785d776881d9d63 (patch) | |
| tree | de0e1e16ae2a1b9d403d0ece0eb5f11eb387a3ad /backends | |
| parent | 137742786e0409a43f9d69177f2929d9226dad8e (diff) | |
| download | yosys-0325efe17214974866be18839785d776881d9d63.tar.gz yosys-0325efe17214974866be18839785d776881d9d63.tar.bz2 yosys-0325efe17214974866be18839785d776881d9d63.zip | |
root bug corrected
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/btor/btor.cc | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index f5babebce..b8ff7bb36 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -415,7 +415,11 @@ struct BtorDumper expr_line, one_line); fprintf(f, "%s\n", str.c_str()); int cell_line = ++line_num; - str = stringf("%d %s %d %d", line_num, cell_type_translation.at("$assert").c_str(), 1, line_num-1); + str = stringf("%d %s %d %d", line_num, cell_type_translation.at("$assert").c_str(), 1, -1*(line_num-1)); + //multiplying the line number with -1, which means logical negation + //the reason for negative sign is that the properties in btor are given as "negation of the original property" + //bug identified by bobosoft + //http://www.reddit.com/r/yosys/comments/1w3xig/btor_backend_bug/ fprintf(f, "%s\n", str.c_str()); line_ref[cell->name]=cell_line; } |