From 268926cb5be57c43cbefd3cd0e67e40770e521a5 Mon Sep 17 00:00:00 2001 From: George Rennie Date: Tue, 8 Oct 2024 14:34:17 +0200 Subject: [PATCH] write_btor: don't emit undriven bits multiple times * Fixes #4640 --- backends/btor/btor.cc | 1 + 1 file changed, 1 insertion(+) diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 9cfd967e581..81402fa498b 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -1077,6 +1077,7 @@ struct BtorWorker btorf("%d input %d\n", nid, sid); ywmap_input(s); nid_width[nid] = GetSize(s); + add_nid_sig(nid, s); for (int j = 0; j < GetSize(s); j++) nidbits.push_back(make_pair(nid, j));