Verilog: wildcards in case items depend on the case kind

[kroening]

Summary

Fixes the KNOWNBUG introduced in #2122. Per IEEE 1800-2017 §12.5.1, the case items of a plain case statement are compared using 4-state equality (===): x and z in a case item are not wildcards. Only casex and casez have wildcards:

• casez treats z (and ?) bits in a case item as wildcards.
• casex treats x, z (and ?) bits in a case item as wildcards.

Previously the case items were masked irrespective of the kind of case statement, i.e., every case was effectively treated like casex.

Changes

• src/verilog/verilog_synthesis.cpp: case_comparison now receives the case-statement kind and selects the wildcard bits accordingly (none for case, z-only for casez, x/z for casex). Non-wildcard positions are compared using 4-state equality (both aval and bval must match), which also correctly handles operands containing x/z. Added a PRECONDITION on the case kind.
• src/verilog/verilog_synthesis_class.h: threaded the case kind through case_comparison and synth_case_values.
• regression/verilog/case/case_wildcard1.desc: KNOWNBUG → CORE.
• regression/verilog/case/case_wildcard2.{sv,desc}: new test locking in the casex vs casez distinction.

Testing

• make -C src builds clean.
• make -C regression/verilog test: all case/*.desc pass, including both wildcard tests; no failures across the suite.
• make -C regression/ebmc test and make -C regression/smv test: no failures.