From 6503624190699a0572b49cadf44cceee97a3e984 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 19 Oct 2025 16:39:14 -0700
Subject: [PATCH] Verilog: fix for port direction of output register ports

Output register ports are now recognised as outputs.  Fixes a regression
introduced by #1271.

Closes #635.
---
 CHANGELOG                              | 1 +
 regression/verilog/modules/ports9.desc | 3 +--
 src/verilog/verilog_interfaces.cpp     | 4 ++++
 3 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/CHANGELOG b/CHANGELOG
index f4e1d66b9..dac3a2f3c 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,6 +1,7 @@
 # EBMC 5.8
 
 * SystemVerilog: cover sequence
+* Verilog: semantic fix for output register ports
 
 # EBMC 5.7
 
diff --git a/regression/verilog/modules/ports9.desc b/regression/verilog/modules/ports9.desc
index 201224631..eeaff0b10 100644
--- a/regression/verilog/modules/ports9.desc
+++ b/regression/verilog/modules/ports9.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ports9.sv
 --bound 1
 ^EXIT=0$
@@ -6,4 +6,3 @@ ports9.sv
 --
 ^warning: ignoring
 --
-This gives the wrong answer.
diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp
index e9ff6f54b..47169a64f 100644
--- a/src/verilog/verilog_interfaces.cpp
+++ b/src/verilog/verilog_interfaces.cpp
@@ -108,6 +108,10 @@ void verilog_typecheckt::check_module_ports(
       else
         direction = ID_inout;
     }
+    else if(direction == ID_output_register)
+    {
+      direction = ID_output;
+    }
 
     ports.emplace_back(identifier, port_symbol->type, direction);