summaryrefslogtreecommitdiff
path: root/test/smt/match_fail_query_1.sat.sail
diff options
context:
space:
mode:
Diffstat (limited to 'test/smt/match_fail_query_1.sat.sail')
-rw-r--r--test/smt/match_fail_query_1.sat.sail10
1 files changed, 10 insertions, 0 deletions
diff --git a/test/smt/match_fail_query_1.sat.sail b/test/smt/match_fail_query_1.sat.sail
new file mode 100644
index 00000000..15036ad9
--- /dev/null
+++ b/test/smt/match_fail_query_1.sat.sail
@@ -0,0 +1,10 @@
+default Order dec
+
+$include <prelude.sail>
+
+$counterexample :query ~(exist match_failure)
+function prop(xs: bits(4)) -> unit = {
+ match xs {
+ _ : bits(3) @ 0b0 => ()
+ }
+}