From 2e605e5993b65f3d3960e95aee84af0316365e3b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 21 Oct 2025 11:47:01 -0700 Subject: [PATCH] Verilog: make power3 test work The test power3.desc uses 'x, which doesn't work right now. The test works when replacing 'x by a sized literal. --- regression/verilog/expressions/power3.desc | 3 +-- regression/verilog/expressions/power3.sv | 8 ++++---- 2 files changed, 5 insertions(+), 6 deletions(-) diff --git a/regression/verilog/expressions/power3.desc b/regression/verilog/expressions/power3.desc index 1eb22c033..7a010c6a3 100644 --- a/regression/verilog/expressions/power3.desc +++ b/regression/verilog/expressions/power3.desc @@ -1,4 +1,4 @@ -KNOWNBUG +CORE broken-smt-backend power3.sv ^EXIT=0$ @@ -6,4 +6,3 @@ power3.sv -- ^warning: ignoring -- -The result is wrong. diff --git a/regression/verilog/expressions/power3.sv b/regression/verilog/expressions/power3.sv index dfc2c3013..c1c976381 100644 --- a/regression/verilog/expressions/power3.sv +++ b/regression/verilog/expressions/power3.sv @@ -1,9 +1,9 @@ module main; // Any arithmetic with x or z returns x. - initial assert('bx ** 1 === 'x); - initial assert('bz ** 1 === 'x); - initial assert(1 ** 'bx === 'x); - initial assert(1 ** 'bz === 'x); + initial assert('bx ** 1 === 32'hxxxx_xxxx); + initial assert('bz ** 1 === 32'hxxxx_xxxx); + initial assert(1 ** 'bx === 32'hxxxx_xxxx); + initial assert(1 ** 'bz === 32'hxxxx_xxxx); endmodule