circt/test/Target/ExportSMTLIB/bitvector-errors.mlir

8 lines
278 B
MLIR

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