File tree Expand file tree Collapse file tree 2 files changed +2
-2
lines changed
Expand file tree Collapse file tree 2 files changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -18,7 +18,7 @@ void assert(_Bool assertion);
1818The function **\_\_CPROVER\_assume** adds an expression as a constraint
1919to the program. If the expression evaluates to false, the execution
2020aborts without failure. More detail on the use of assumptions is in the
21- section on [Assumptions](./modeling- assumptions.md ).
21+ section on [Assumptions](.. /modeling/ assumptions/ ).
2222
2323#### \_\_CPROVER\_r_ok, \_\_CPROVER\_w_ok
2424
Original file line number Diff line number Diff line change @@ -33,7 +33,7 @@ properties together with the condition.
3333
3434The assertion language of the CPROVER tools is identical to the language
3535used for expressions. Note that
36- [nondeterminism](./ modeling- nondeterminism.md ) can be exploited in order
36+ [nondeterminism](../../ modeling/ nondeterminism/ ) can be exploited in order
3737to check a range of choices. As an example, the following code fragment
3838asserts that **all** elements of the array are zero:
3939
You can’t perform that action at this time.
0 commit comments