From d11cc34cb3c619962229bb6a31cbe1160e1f41e0 Mon Sep 17 00:00:00 2001
From: "N. Engelhardt" <nak@yosyshq.com>
Date: Mon, 6 Jul 2026 19:58:52 +0200
Subject: [PATCH] fix aiger witness handling for combinational designs (empty
 newlines are semantically important for aiw output parsed from log)

---
 sbysrc/sby_core.py                      |  9 +++++++--
 sbysrc/sby_engine_aiger.py              |  2 ++
 tests/regression/aiger_comb_witness.sby | 21 +++++++++++++++++++++
 3 files changed, 30 insertions(+), 2 deletions(-)
 create mode 100644 tests/regression/aiger_comb_witness.sby

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index aeb9b21..d97599c 100644
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -91,6 +91,7 @@ class SbyProc:
         self.noprintregex = None
         self.notify = []
         self.linebuffer = ""
+        self.preserve_whitespace = False
         self.logstderr = logstderr
         self.silent = silent
         self.wait = False
@@ -125,7 +126,7 @@ class SbyProc:
             self.task.log(f"{click.style(self.info, fg='magenta')}: {line}")
 
     def handle_output(self, line):
-        if self.terminated or len(line) == 0:
+        if self.terminated or (len(line) == 0 and not self.preserve_whitespace):
             return
         if self.output_callback is not None:
             line = self.output_callback(line)
@@ -296,7 +297,11 @@ class SbyProc:
             if outs[-1] != '\n':
                 self.linebuffer += outs
                 break
-            outs = (self.linebuffer + outs).strip()
+            outs = self.linebuffer + outs
+            if self.preserve_whitespace:
+                outs = outs.rstrip("\r\n")
+            else:
+                outs = outs.strip()
             self.linebuffer = ""
             self.handle_output(outs)
 
diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py
index 703da8e..ce9d169 100644
--- a/sbysrc/sby_engine_aiger.py
+++ b/sbysrc/sby_engine_aiger.py
@@ -106,6 +106,8 @@ def run(mode, task, engine_idx, engine):
     )
     if solver_args[0] not in ["avy", "rIC3"]:
         proc.checkretcode = True
+    if not json_output:
+        proc.preserve_whitespace = True
 
     proc_status = None
     produced_cex = False
diff --git a/tests/regression/aiger_comb_witness.sby b/tests/regression/aiger_comb_witness.sby
new file mode 100644
index 0000000..3458673
--- /dev/null
+++ b/tests/regression/aiger_comb_witness.sby
@@ -0,0 +1,21 @@
+[tasks]
+aigbmc
+ric3
+
+[options]
+mode bmc
+depth 1
+expect fail
+
+[engines]
+aigbmc: aiger aigbmc
+ric3: aiger rIC3
+
+[script]
+read -formal top.sv
+prep -top top
+
+[file top.sv]
+module top(input a);
+    always @* assert (!a);
+endmodule