From: Ahmed Irfan <ahmedirfan1983@gmail.com>
Date: Sat, 25 Jan 2014 18:33:24 +0000 (+0100)
Subject: root bug corrected
X-Git-Tag: yosys-0.2.0~146^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0325efe17214974866be18839785d776881d9d63;p=yosys.git

root bug corrected
---

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;
 			}