SVA: type checking for SVA not

This fixes the type checking for the SVA not operator.

Author: kroening

regression/verilog/SVA/sva_not1.desc

@@ -0,0 +1,9 @@
+CORE
+sva_not1.sv
+--k-induction
+^\[main\.p0] always not 0: PROVED$
+^\[main\.p1] always not 1: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/SVA/sva_not1.sv

@@ -0,0 +1,9 @@
+module main;
+
+  // should pass
+  p0: assert property (not 0);
+
+  // should fail
+  p1: assert property (not 1);
+
+endmodule

src/verilog/verilog_typecheck_expr.cpp

@@ -2270,7 +2270,8 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     convert_expr(expr.op());
 
     if (expr.op().type().id() == ID_verilog_signedbv ||
-        expr.op().type().id() == ID_verilog_unsignedbv) {
+        expr.op().type().id() == ID_verilog_unsignedbv)
+    {
       expr.type()=verilog_unsignedbv_typet(1);
     }
     else
@@ -2279,6 +2280,13 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
       make_boolean(expr.op());
     }
   }
+  else if(expr.id() == ID_sva_not)
+  {
+    convert_expr(expr.op());
+    make_boolean(expr.op());
+    expr.type()=bool_typet(); // always boolean, never x
+    return std::move(expr);
+  }
   else if(expr.id()==ID_reduction_or  || expr.id()==ID_reduction_and ||
           expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
           expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor)