Repository navigation
[MLIR][SMT] isa<SMTDialect>(op->getDialect()) asserts on an unregistered op inside smt.exists/smt.forall patterns and transform.smt.constrain_params (--allow-unregistered-dialect) #239942
Description
The following code:
module attributes {transform.with_named_sequence} {
transform.named_sequence @s(%arg0: !transform.any_op {transform.readonly}) {
%p = transform.param.constant 42 -> !transform.param<i64>
transform.smt.constrain_params(%p) : (!transform.param<i64>) -> () {
^bb0(%v: !smt.int):
"foo.bar"() : () -> ()
}
transform.yield
}
}
// -----
func.func @f() {
%0 = smt.exists ["a"] {
^bb0(%a: !smt.int):
%c = smt.int.constant 0
%e = smt.eq %a, %c : !smt.int
smt.yield %e : !smt.bool
} patterns {
^bb0(%a: !smt.int):
"foo.bar"() : () -> ()
smt.yield %a : !smt.int
}
return
}Resulted in this output:
Program terminated with signal SIGSEGV (11)
Stack dump:
#3 mlir::transform::smt::ConstrainParamsOp::verify
#4 mlir::RegisteredOperationName::Model::verifyInvariants
#5 (anonymous namespace)::OperationVerifier::verifyOnEntrance
#6 (anonymous namespace)::OperationVerifier::verifyOperation
#7 (anonymous namespace)::OperationVerifier::verifyOperation
#8 (anonymous namespace)::OperationVerifier::verifyOperation
#9 mlir::verify
#10 mlir::parseAsmSourceFile
Trunk reproducer (--split-input-file --allow-unregistered-dialect): https://godbolt.org/z/vnKe9nfW3
Activity
llvmorg-github-actions commentedon Nov 7, 2026
@llvm/issue-subscribers-mlir
Author: Jiang Yuancheng (YuanchengJiang)
Details
The following code: ```mlir module attributes {transform.with_named_sequence} { transform.named_sequence @s(%arg0: !transform.any_op {transform.readonly}) { %p = transform.param.constant 42 -> !transform.param<i64> transform.smt.constrain_params(%p) : (!transform.param<i64>) -> () { ^bb0(%v: !smt.int): "foo.bar"() : () -> () } transform.yield } } // ----- func.func @f() { %0 = smt.exists ["a"] { ^bb0(%a: !smt.int): %c = smt.int.constant 0 %e = smt.eq %a, %c : !smt.int smt.yield %e : !smt.bool } patterns { ^bb0(%a: !smt.int): "foo.bar"() : () -> () smt.yield %a : !smt.int } return } ```Resulted in this output:
Trunk reproducer (
--split-input-file --allow-unregistered-dialect): https://godbolt.org/z/vnKe9nfW3