diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 48da3f4be..0ca3fbcac 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -626,9 +626,12 @@ struct Smt2Worker
 				}
 
 				bool init_only = cell->type.in(ID($anyconst), ID($anyinit), ID($allconst));
-				for (auto chunk : cell->getPort(QY).chunks())
+				int smtoffset = 0;
+				for (auto chunk : cell->getPort(QY).chunks()) {
 					if (chunk.is_wire())
-						decls.push_back(witness_signal(init_only ? "init" : "seq", chunk.width, chunk.offset, "", idcounter, chunk.wire));
+						decls.push_back(witness_signal(init_only ? "init" : "seq", chunk.width, chunk.offset, "", idcounter, chunk.wire, smtoffset));
+					smtoffset += chunk.width;
+				}
 
 				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(QY)), log_signal(cell->getPort(QY)));
 				if (cell->type == ID($anyseq))
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index fe1635249..273e9db86 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -223,7 +223,8 @@ struct SimInstance
 
 			if (wire->port_input && instance != nullptr && parent != nullptr) {
 				for (int i = 0; i < GetSize(sig); i++) {
-					in_parent_drivers.emplace(sig[i], parent->sigmap(instance->getPort(wire->name)[i]));
+					if (instance->hasPort(wire->name))
+						in_parent_drivers.emplace(sig[i], parent->sigmap(instance->getPort(wire->name)[i]));
 				}
 			}
 		}