summaryrefslogtreecommitdiff
path: root/backends/btor/btor.cc
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-01-26 02:29:19 +0100
committerClifford Wolf <clifford@clifford.at>2014-01-26 02:29:19 +0100
commitfa103e55ad24ee32c58ded660979c81980d14ab1 (patch)
treed057c5b0993fd5f4b6c527214fdda9b0b285c84c /backends/btor/btor.cc
parentfd6ca84f3ccd5f86ca8aae8215b2ccf38f8f2201 (diff)
parent0325efe17214974866be18839785d776881d9d63 (diff)
Merge branch 'btor' of https://github.com/ahmedirfan1983/yosys
Diffstat (limited to 'backends/btor/btor.cc')
-rw-r--r--backends/btor/btor.cc6
1 files changed, 5 insertions, 1 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index f5babebc..b8ff7bb3 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;
}