diff --git a/src/util/std_expr.cpp b/src/util/std_expr.cpp index 3b95e3e96b9..e78505633c9 100644 --- a/src/util/std_expr.cpp +++ b/src/util/std_expr.cpp @@ -36,13 +36,17 @@ void constant_exprt::check(const exprt &expr, const validation_modet vm) vm, !can_cast_type(expr.type()) || can_cast_type(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(expr.type()) || value == ID_0 || + !can_cast_type(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"); }