From 10d5d358d2b8f82767953e7c5be44637a245582b Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Thu, 11 Jan 2024 14:10:25 +0100
Subject: [PATCH] Ignore $scopeinfo in write_aiger

While SBY's aiger flow already removes non-assertion driving logic,
there are some uses of write_aiger outside of SBY that could end up with
$scopeinfo cells, so we explicitly ignore them.

The write_btor backend works differently and due to the way it
recursively visits cells, it would never reach isolated cells like
$scopeinfo.
---
 backends/aiger/aiger.cc | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index f77a64978..fe4f7681d 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -320,6 +320,9 @@ struct AigerWriter
 				continue;
 			}
 
+			if (cell->type == ID($scopeinfo))
+				continue;
+
 			log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
 		}