diff --git a/regression/verilog/expressions/wildcard_equality1.desc b/regression/verilog/expressions/wildcard_equality1.desc index 6d9359abc..302a4fdfc 100644 --- a/regression/verilog/expressions/wildcard_equality1.desc +++ b/regression/verilog/expressions/wildcard_equality1.desc @@ -9,9 +9,9 @@ wildcard_equality1.sv ^\[main\.property06\] always 2'b10 ==\? 2'b0x === 0: PROVED .*$ ^\[main\.property07\] always 2'b00 !=\? 2'b0x === 0: PROVED .*$ ^\[main\.property08\] always 2'b10 !=\? 2'b0x === 1: PROVED .*$ -^\[main\.property09\] always 2'b11 ==\? 2'b11 === 0: REFUTED$ +^\[main\.property09\] always 1'sb1 ==\? 2'b11 === 0: PROVED .*$ ^\[main\.property10\] always 2'sb11 ==\? 2'sb11 === 1: PROVED .*$ -^EXIT=10$ +^EXIT=0$ ^SIGNAL=0$ -- ^warning: ignoring diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index c56a14b5c..3ad03f859 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/src/verilog/verilog_typecheck_expr.cpp @@ -3262,10 +3262,7 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr) expr.id() == ID_verilog_wildcard_inequality) { // ==? and !=? - Forall_operands(it, expr) - convert_expr(*it); - - tc_binary_expr(expr); + convert_relation(expr); expr.type() = verilog_unsignedbv_typet(1);