diff --git a/regression/verilog/primitive_gates/or1.desc b/regression/verilog/primitive_gates/or1.desc
new file mode 100644
index 000000000..957d6228e
--- /dev/null
+++ b/regression/verilog/primitive_gates/or1.desc
@@ -0,0 +1,10 @@
+KNOWNBUG
+or1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This is a small version of a misencoding of the Verilog primitive gates
+reported as https://github.com/diffblue/hw-cbmc/issues/880
diff --git a/regression/verilog/primitive_gates/or1.sv b/regression/verilog/primitive_gates/or1.sv
new file mode 100644
index 000000000..8cce5522f
--- /dev/null
+++ b/regression/verilog/primitive_gates/or1.sv
@@ -0,0 +1,16 @@
+module main(input or_in1, or_in2, or_in3);
+
+  wire  or_out;
+
+  or o1(or_out, or_in1, or_in2, or_in3);
+
+  // should pass
+  or_ok: assert final ((or_in1 || or_in2 || or_in3)==or_out);
+
+  // should fail
+  or_not_ok1: assert final (or_out == (or_in1 || or_in2));
+
+  // should fail
+  or_not_ok2: assert final (or_in1 || or_in2 || !or_in3);
+
+endmodule