84 lines · plain
1// RUN: mlir-translate --export-smtlib %s --split-input-file --verify-diagnostics2 3smt.solver () : () -> () {4 %0 = smt.constant true5 // expected-error @below {{must not have any result values}}6 %1 = smt.check sat {7 smt.yield %0 : !smt.bool8 } unknown {9 smt.yield %0 : !smt.bool10 } unsat {11 smt.yield %0 : !smt.bool12 } -> !smt.bool13}14 15// -----16 17smt.solver () : () -> () {18 // expected-error @below {{'sat' region must be empty}}19 smt.check sat {20 %0 = smt.constant true21 smt.yield22 } unknown {23 } unsat {24 }25}26 27// -----28 29smt.solver () : () -> () {30 // expected-error @below {{'unknown' region must be empty}}31 smt.check sat {32 } unknown {33 %0 = smt.constant true34 smt.yield35 } unsat {36 }37}38 39// -----40 41smt.solver () : () -> () {42 // expected-error @below {{'unsat' region must be empty}}43 smt.check sat {44 } unknown {45 } unsat {46 %0 = smt.constant true47 smt.yield48 }49}50 51// -----52 53// expected-error @below {{solver scopes with inputs or results are not supported}}54%0 = smt.solver () : () -> (i1) {55 %1 = arith.constant true56 smt.yield %1 : i157}58 59// -----60 61smt.solver () : () -> () {62 // expected-error @below {{solver must not contain any non-SMT operations}}63 %1 = arith.constant true64}65 66// -----67 68func.func @solver_input(%arg0: i1) {69 // expected-error @below {{solver scopes with inputs or results are not supported}}70 smt.solver (%arg0) : (i1) -> () {71 ^bb0(%arg1: i1):72 smt.yield73 }74 return75}76 77// -----78 79smt.solver () : () -> () {80 %0 = smt.declare_fun : !smt.sort<"uninterpreted0">81 // expected-error @below {{uninterpreted sorts with same identifier but different arity found}}82 %1 = smt.declare_fun : !smt.sort<"uninterpreted0"[!smt.bool]>83}84