| | 447 | The system function `$assume` has signature |
| | 448 | {{{ |
| | 449 | void $assume(_Bool expr); |
| | 450 | }}} |
| | 451 | During verification, the given expression is assumed to hold. If this leads to a contradiction on some execution, that execution is simply ignored. It never reports a violation, it only restricts the set of possible executions that will be explored by the verification algorithm. |
| | 452 | Like an assertion call, an assume call can be used any place a statement is expected. In addition, an assume call can be used in file scope to place restrictions on the global variables of the programs. For example, |
| | 453 | {{{ |
| | 454 | $input int B, N; |
| | 455 | $assume(1<=N && N<=B); |
| | 456 | }}} |
| | 457 | declares `N` and `B` to be integer inputs and restricts consideration to inputs satisfying 1 ≤ `N` ≤ `B`. |
| | 458 | |
