diff --git a/tests/verilog/issue4402.ys b/tests/verilog/issue4402.ys
new file mode 100644
index 000000000..82133f60e
--- /dev/null
+++ b/tests/verilog/issue4402.ys
@@ -0,0 +1,20 @@
+# Issue #4402: read_verilog doesn't respect signed keyword
+#
+# write_verilog drops the signed keyword from input port declarations,
+# even though the internal comparison logic is correctly preserved via
+# explicit $signed() casts. The port declaration should retain signed
+# so that the interface contract is correct for downstream tools.
+
+! mkdir -p temp
+
+read_verilog <<EOT
+module mod (output k, input signed [5:0] wire0);
+  assign k = (wire0 <= 0);
+endmodule
+EOT
+hierarchy -top mod
+write_verilog temp/issue4402_roundtrip.v
+
+# The output port declaration must include the signed keyword.
+# Bug: write_verilog emits `input [5:0] wire0` instead of `input signed [5:0] wire0`.
+! grep -q "input signed" temp/issue4402_roundtrip.v
diff --git a/tests/verilog/issue5745.ys b/tests/verilog/issue5745.ys
new file mode 100644
index 000000000..1e16b8373
--- /dev/null
+++ b/tests/verilog/issue5745.ys
@@ -0,0 +1,18 @@
+# Issue #5745: chparam values are unsigned when using read_verilog frontend
+#
+# When chparam overrides a parameter value, the signed attribute is lost,
+# causing signed comparisons to silently use unsigned logic.
+#
+# m = -32 (signed 9-bit), p2 = 11. Correct signed semantics: -32 < 11, so k = 1.
+# Bug: chparam strips the signed attribute from p2. The $lt cell gets A_SIGNED=0,
+# B_SIGNED=0, so the comparison treats m as unsigned (480 > 11), giving k = 0.
+
+read_verilog <<EOT
+module mod #(parameter p2=11) (output k);
+  wire signed [8:0] m = -32;
+  assign k = m < p2;
+endmodule
+EOT
+chparam -set p2 11
+hierarchy -top mod
+sat -prove k 1 -verify