From 3730db4b986fd69941a16520cfd54179a3424d0e Mon Sep 17 00:00:00 2001
From: Miodrag Milanovic <mmicko@gmail.com>
Date: Mon, 2 May 2022 11:18:30 +0200
Subject: [PATCH] AIM file could have gaps in or between inputs and inits

---
 passes/sat/sim.cc | 9 ++++++---
 1 file changed, 6 insertions(+), 3 deletions(-)

diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 5f795e94c..7b52b85cd 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -1798,6 +1798,7 @@ struct AIWWriter : public OutputWriter
 		std::ifstream mf(worker->map_filename);
 		std::string type, symbol;
 		int variable, index;
+		int max_input = 0;
 		if (mf.fail())
 			log_cmd_error("Not able to read AIGER witness map file.\n");
 		while (mf >> type >> variable >> index >> symbol) {
@@ -1815,8 +1816,10 @@ struct AIWWriter : public OutputWriter
 				if (worker->clockn.count(escaped_s)) {
 					clocks[variable] = false;
 				}
+				max_input = max(max_input,variable);
 			} else if (type == "init") {
 				aiw_inits[variable] = SigBit(w,index-w->start_offset);
+				max_input = max(max_input,variable);
 			} else if (type == "latch") {
 				aiw_latches[variable] = {SigBit(w,index-w->start_offset), false};
 			} else if (type == "invlatch") {
@@ -1863,7 +1866,7 @@ struct AIWWriter : public OutputWriter
 			}
 			if (skip)
 				continue;
-			for (int i = 0;; i++)
+			for (int i = 0; i <= max_input; i++)
 			{
 				if (aiw_inputs.count(i)) {
 					SigBit bit = aiw_inputs.at(i);
@@ -1883,9 +1886,9 @@ struct AIWWriter : public OutputWriter
 						aiwfile << '0';
 					continue;
 				}
-				aiwfile << '\n';
-				break;
+				aiwfile << '0';
 			}
+			aiwfile << '\n';
 		} 
 	}
 
-- 
2.30.2