# W7001 property_discard_budget

URL: /docs/errors/W7001
Markdown: /docs/errors/W7001.md

> A property discarded more than 90% of its generated inputs, so it tested almost nothing (design §7.4, §17.64).

A warning from the `verify` phase. `sakura explain W7001` prints this explanation offline.

A property discarded more than 90% of its generated inputs, so it tested almost nothing
(design §7.4, §17.64). For a property synthesized by `sakura test --contracts`, inputs come from
the parameter types and `requires`: ranges, lengths, enums and non-empty lists are generated
directly, anything else is a filter. The test fails rather than passing vacuously. Restate the
parameters so the generator builds valid inputs.

Warning (under `sakura test --contracts`):

```sakura
pub fn sku(code: String) -> String
  requires String.starts_with(code, "SKU-")
{ code }
```

Fixed (a range the generator constructs):

```sakura
pub fn sku(number: Int) -> String
  requires number >= 0
{ "SKU-{number}" }
```

## Wrong program [#wrong-program]

[`compiler/tests/ui/W7001_property_discard_budget.sakura`](https://github.com/icantcodefyi/sakuralang/blob/master/compiler/tests/ui/W7001_property_discard_budget.sakura), which the compiler's ui suite runs through `sakura test --contracts`:

```sakura
pub fn exact(x: Int) -> Int
  requires x == 123_456
{ x }
```

`sakura test --contracts` reports `W7001`.

## Fixed program [#fixed-program]

[`compiler/tests/ui/W7001_property_discard_budget.fixed.sakura`](https://github.com/icantcodefyi/sakuralang/blob/master/compiler/tests/ui/W7001_property_discard_budget.fixed.sakura), which `sakura test --contracts` accepts with no diagnostics:

```sakura
pub fn exact(x: Int) -> Int
  requires x >= 0 && x <= 123_456
{ x }
```