test/smt/match_fail_query_1.sat.sail


1
2
3
4
5
6
7
8
9
10

default Order dec

$include <prelude.sail>

$counterexample :query ~(exist match_failure)
function prop(xs: bits(4)) -> unit = {
  match xs {
    _ : bits(3) @ 0b0 => ()
  }
}