llvm-project/mlir/test/Target/SMTLIB/integer-errors.mlir
Maksim Levental acf964b95f
[mlir][SMT] add export smtlib (#131492)
This PR adds the `ExportSMTLIB` translation/egress pass for `SMT`
dialect.
2025-04-12 16:39:16 -04:00

8 lines
247 B
MLIR

// RUN: mlir-translate --export-smtlib %s --split-input-file --verify-diagnostics
smt.solver () : () -> () {
%0 = smt.int.constant 5
// expected-error @below {{operation not supported for SMTLIB emission}}
%1 = smt.int2bv %0 : !smt.bv<4>
}