fix aiger witness handling for combinational designs (empty newlines are semantically important for aiw output parsed from log)

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)
 

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

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