integer-errors.mlir « SMTLIB « Target « test « mlir - llvm-project.git - Unnamed repository; edit this file 'description' to name the repository.

index : llvm-project.git

Unnamed repository; edit this file 'description' to name the repository.

thomasg

summary refs log tree commit diff

path: root/mlir/test/Target/SMTLIB/integer-errors.mlir

blob: 4dc5f48f4fe5b947dbd6ca416c9d1ecbffdb7365 (plain)

// 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>
}