add symbolic instructions in the README

README.md

@@ -16,6 +16,8 @@ If you can't or don't want to use `opam`, you can build the package with `dune b
 
 ## Quickstart
 
+### Concrete interpretation
+
 Given a file `test/passing/quickstart.wast` with the following content:
 
 <!-- $MDX file=test/passing/quickstart.wast -->
@@ -102,6 +104,21 @@ stack        : [  ]
 
 For more, have a look at the [example] folder, at the [documentation] or at the [test suite].
 
+### Symbolic interpretation
+
+The interpreter can also be used in symbolic mode. This allows to find which input values are leading to a trap.
+
+Given a file `test/mini_test.wast` with the following content:
+
+<!-- $MDX file=test/mini_test.wast -->
+```wast
+```
+
+You can run the symbolic interpreter through the `sym` command:
+```sh
+$ dune exec owi -- sym test/mini_test.wast
+```
+
 ## Supported proposals
 
 The 🐌 status means the proposal is not applicable to owi.

test/mini_test.wast

@@ -18,7 +18,7 @@
     (local $x i32)
     (i32.const 123)
     (call $print_i32)
-    (local.set $x (call $gen_i32 (i32.const 1)))
+    (local.set $x (call $gen_i32 (i32.const 42)))
     (if (i32.lt_s (i32.const 5) (local.get $x)) (then
       unreachable
     ))