Verilog: KNOWNBUG for primitive gates with more than two inputs

This replicates issue #880.

Author: kroening

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

regression/verilog/primitive_gates/or1.sv

@@ -0,0 +1,13 @@
+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_ok: assert final (or_out == (or_in1 || or_in2));
+
+endmodule

src/verilog/verilog_synthesis.cpp

@@ -1586,17 +1586,21 @@ void verilog_synthesist::synth_module_instance_builtin(
     {
       assert(instance.connections().size() >= 2);
 
-      for(unsigned i = 0; i < instance.connections().size() - 1; i++)
-      {
-        exprt op(ID_not, instance.type());
-        op.add_to_operands(instance.connections()[i]);
+      // May have multiple outputs. The input is the last connection.
+      auto &input = instance.connections().back();
+      exprt rhs;
 
-        if(instance.type().id()!=ID_bool)
-          op.id("bit"+op.id_string());
-
-        equal_exprt constraint{op, instance.connections().back()};
+      if(input.type().id() == ID_bool)
+        rhs = not_exprt{input};
+      else
+        rhs = bitnot_exprt{input};
 
-        assert(trans.operands().size()==3);
+      rhs.add_source_location() = module_item.source_location();
+      
+      for(std::size_t i = 0; i < instance.connections().size() - 1; i++)
+      {
+        auto &lhs = instance.connections()[i];
+        auto constraint = equal_exprt{lhs, rhs};
         trans.invar().add_to_operands(std::move(constraint));
       }
     }