From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 8 Dec 2018 05:21:31 +0000 (+0100)
Subject: Fix btor init value handling
X-Git-Tag: yosys-0.9~389
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ed3c57fad3616b981e54e2f209e7ee40ff87c8a7;p=yosys.git

Fix btor init value handling

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 58d2a8625..ab2702807 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -506,6 +506,18 @@ struct BtorWorker
 				}
 			}
 
+			Const initval;
+			for (int i = 0; i < GetSize(sig_q); i++)
+				if (initbits.count(sig_q[i]))
+					initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0);
+				else
+					initval.bits.push_back(State::Sx);
+
+			int nid_init_val = -1;
+
+			if (!initval.is_fully_undef())
+				nid_init_val = get_sig_nid(initval);
+
 			int sid = get_bv_sid(GetSize(sig_q));
 			int nid = next_nid++;
 
@@ -514,15 +526,7 @@ struct BtorWorker
 			else
 				btorf("%d state %d %s\n", nid, sid, log_id(symbol));
 
-			Const initval;
-			for (int i = 0; i < GetSize(sig_q); i++)
-				if (initbits.count(sig_q[i]))
-					initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0);
-				else
-					initval.bits.push_back(State::Sx);
-
-			if (!initval.is_fully_undef()) {
-				int nid_init_val = get_sig_nid(initval);
+			if (nid_init_val >= 0) {
 				int nid_init = next_nid++;
 				if (verbose)
 					btorf("; initval = %s\n", log_signal(initval));