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,71 @@ 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
+(module
+  (import "print" "i32" (func $print_i32 (param i32)))
+  (import "symbolic" "i32" (func $gen_i32 (param i32) (result i32)))
+  (func $factR (export "fact") (param $n i32) (result i32)
+    local.get $n
+    local.get $n
+    i32.const 1
+    i32.eq
+    br_if 0
+    i32.const 1
+    i32.sub
+    call $factR
+    local.get $n
+    i32.mul
+  )
+
+  (func $start
+    (local $x i32)
+    (i32.const 123)
+    (call $print_i32)
+    (local.set $x (call $gen_i32 (i32.const 42)))
+    (if (i32.lt_s (i32.const 5) (local.get $x)) (then
+      unreachable
+    ))
+    (if (i32.gt_s (i32.const 1) (local.get $x)) (then
+      unreachable
+    ))
+    (local.get $x)
+    (call $factR)
+    (call $print_i32))
+
+  (start $start)
+)
+```
+
+You can run the symbolic interpreter through the `sym` command:
+```sh
+$ dune exec owi -- sym test/mini_test.wast
+(i32 123)
+CHOICE: (i32.lt_s (i32 5) x_1)
+PATH CONDITION:
+(i32.lt_s (i32 5) x_1)
+TRAP: unreachable
+CHOICE: (i32.gt_s (i32 1) x_1)
+CHOICE: (i32.eq x_1 (i32 1))
+Model:
+(model
+(x_1 i32 (i32 6))
+)
+Reached problem!
+
+x_1
+Solver time 0.003568s
+      calls 1
+  mean time 3.568000ms
+```
+
 ## 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
     ))