Merge pull request #8191 from diffblue/bitvector-constant-verilogbv

relax bitvector constant check for Verilog bitvectors

Author: kroening

src/util/std_expr.cpp

@@ -36,13 +36,17 @@ void constant_exprt::check(const exprt &expr, const validation_modet vm)
     vm,
     !can_cast_type<bitvector_typet>(expr.type()) ||
       can_cast_type<pointer_typet>(expr.type()) ||
+      expr.type().id() == ID_verilog_unsignedbv ||
+      expr.type().id() == ID_verilog_signedbv ||
       id2string(value).find_first_not_of("0123456789ABCDEF") ==
         std::string::npos,
     "negative bitvector constant must use two's complement");
 
   DATA_CHECK(
     vm,
-    !can_cast_type<bitvector_typet>(expr.type()) || value == ID_0 ||
+    !can_cast_type<bitvector_typet>(expr.type()) ||
+      expr.type().id() == ID_verilog_unsignedbv ||
+      expr.type().id() == ID_verilog_signedbv || value == ID_0 ||
       id2string(value)[0] != '0',
     "bitvector constant must not have leading zeros");
 }