Skip to content

Commit

Permalink
Determinist c/Readme.md
Browse files Browse the repository at this point in the history
  • Loading branch information
krtab committed Mar 4, 2024
1 parent d17beb3 commit 8902770
Show file tree
Hide file tree
Showing 2 changed files with 4 additions and 4 deletions.
6 changes: 3 additions & 3 deletions example/c/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -31,16 +31,16 @@ We are defining one symbolic variable `x` using the function `owi_i32(void)`. Th
Then we use `owi_assert(poly != 0)`. Which should fail as this polynomial has multiple roots. Let's see what owi says about it:

```sh
$ dune exec owi -- c ./poly.c
$ dune exec owi -- c ./poly.c -w1
...
Model:
(model
(symbol_0 (i32 1)))
(symbol_0 (i32 2)))
Reached problem!
[13]
```

Indeed, `1` is a root of the polynomial and thus it is expected to be equal to `0` in this case. We know the three roots are `1`, `2` and `4`, so let's inform owi that we are not interested in this cases.
Indeed, `2` is a root of the polynomial and thus it is expected to be equal to `0` in this case. We know the three roots are `1`, `2` and `4`, so let's inform owi that we are not interested in this cases.

We can do so by assuming that `x` is not equal to any of these with the function `owi_assume(bool)`:

Expand Down
2 changes: 1 addition & 1 deletion example/define_host_function/dune
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
(libraries owi))

(mdx
(libraries owi)
(libraries owi fpath)
(deps
%{bin:owi}
(file extern.exe)
Expand Down

0 comments on commit 8902770

Please sign in to comment.