8 lines · plain
1// RUN: mlir-translate --export-smtlib %s --split-input-file --verify-diagnostics2 3smt.solver () : () -> () {4 %0 = smt.int.constant 55 // expected-error @below {{operation not supported for SMTLIB emission}}6 %1 = smt.int2bv %0 : !smt.bv<4>7}8