[Mlir-commits] [mlir] [mlir][SMT] upstream `SMT` dialect (PR #131480)

[Martin Erhart]

maerhart wrote:

> Do you think we should have a verifier for ConcatOp as well? To make sure that the result width is equal to the sum of all input widths.

The `InferTypeOpInterface` specifies a verifies that checks that the actual result type matches the inferred result type. There is also a test for that specific case in `bitvector-errors.mlir`.

Interesting that `comb.concat` redundantly specifies a verifier. That should get fixed, thanks for pointing it out!

https://github.com/llvm/llvm-project/pull/131480