diff --git a/CHANGES.md b/CHANGES.md
index 3cbb9677f..4ccde8b23 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,7 +1,7 @@
 ## unreleased
 
 - parameterize the `Thread` module on the symbolic memory and the `Choice_monad` module on a Thread
-- adds a `owi_char` function to create char symbolic value
+- add `owi_char` and `owi_bool` function to create char and bool symbolic values
 - adds a `Mem` argument to external function to allow direct manipulation of the memory.
 - support other solvers through the `--solver` option (Z3, Colibri2, Bitwuzla and CVC5)
 - support the extended constant expressions proposal
diff --git a/src/concolic/concolic_wasm_ffi.ml b/src/concolic/concolic_wasm_ffi.ml
index abc4ed679..b5db968b3 100644
--- a/src/concolic/concolic_wasm_ffi.ml
+++ b/src/concolic/concolic_wasm_ffi.ml
@@ -86,6 +86,18 @@ module M :
         let n = Float64.of_bits n in
         (F64 n, Value.pair n (Expr.mk_symbol sym)) )
 
+  let symbol_bool () : Value.int32 Choice.t =
+    Choice.with_new_symbol Ty_bool (fun sym forced_value ->
+        let b =
+          match forced_value with
+          | None -> Random.bool ()
+          | Some True -> true
+          | Some False -> false
+          | _ -> assert false
+        in
+        let n = V.Bool.int32 b in
+        (I32 n, Value.(Bool.int32 (pair b (Expr.mk_symbol sym)))) )
+
   let assume_i32 (i : Value.int32) : unit Choice.t =
     let c = Value.I32.to_bool i in
     Concolic_choice.assume c
@@ -157,6 +169,9 @@ let symbolic_extern_module =
     ; ( "f64_symbol"
       , Concolic.P.Extern_func.Extern_func (Func (UArg Res, R1 F64), symbol_f64)
       )
+    ; ( "bool_symbol"
+      , Concolic.P.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_bool)
+      )
     ; ( "assume"
       , Concolic.P.Extern_func.Extern_func
           (Func (Arg (I32, Res), R0), assume_i32) )
diff --git a/src/intf/wasm_ffi_intf.ml b/src/intf/wasm_ffi_intf.ml
index 04c39052c..bb2a691f3 100644
--- a/src/intf/wasm_ffi_intf.ml
+++ b/src/intf/wasm_ffi_intf.ml
@@ -29,6 +29,8 @@ module type S0 = sig
 
   val symbol_f64 : unit -> Value.float64 t
 
+  val symbol_bool : unit -> Value.int32 t
+
   val assume_i32 : Value.int32 -> unit t
 
   val assume_positive_i32 : Value.int32 -> unit t
diff --git a/src/libc/src/test-comp.c b/src/libc/src/test-comp.c
index 15a8c76e2..b5c82fd71 100644
--- a/src/libc/src/test-comp.c
+++ b/src/libc/src/test-comp.c
@@ -1,17 +1,7 @@
 #include <owi.h>
 
-static __attribute__((naked,noinline,optnone)) _Bool or_(_Bool a, _Bool b) {
-  __asm__ __volatile__("local.get 0;"
-                       "local.get 1;"
-                       "i32.or;"
-                       "return;");
-}
-
 _Bool __VERIFIER_nondet_bool(void) {
-  const _Bool var = owi_i32();
-  const _Bool pc = or_(var == 0, var == 1);
-  owi_assume(pc);
-  return var;
+  return owi_bool();
 }
 
 char __VERIFIER_nondet_char(void) { return (char)owi_i32(); }
diff --git a/src/symbolic/symbolic_value.ml b/src/symbolic/symbolic_value.ml
index c3ee37722..f97f4a3ad 100644
--- a/src/symbolic/symbolic_value.ml
+++ b/src/symbolic/symbolic_value.ml
@@ -200,6 +200,7 @@ module I32 = struct
   let to_bool (e : vbool) =
     match view e with
     | Val (Num (I32 i)) -> Bool.const @@ Int32.ne i 0l
+    | Symbol { ty = Ty_bool; _ } -> e
     | Cvtop (_, OfBool, cond) -> cond
     | _ -> make (Cvtop (ty, ToBool, e))
 
diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml
index 3999eb902..75500ec8c 100644
--- a/src/symbolic/symbolic_wasm_ffi.ml
+++ b/src/symbolic/symbolic_wasm_ffi.ml
@@ -27,6 +27,10 @@ module M :
   let assert_i32 (i : Value.int32) : unit Choice.t =
     Choice.assertion @@ Value.I32.to_bool i
 
+  let symbol_bool () =
+    Choice.with_new_symbol (Ty_bitv 1) (fun sym ->
+        Expr.cvtop (Ty_bitv 32) (Smtml.Ty.Zero_extend 31) (Expr.symbol sym) )
+
   let symbol_i8 () =
     Choice.with_new_symbol (Ty_bitv 8) (fun sym ->
         Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) )
@@ -78,6 +82,9 @@ let symbolic_extern_module =
     ; ( "f64_symbol"
       , Symbolic.P.Extern_func.Extern_func (Func (UArg Res, R1 F64), symbol_f64)
       )
+    ; ( "bool_symbol"
+      , Symbolic.P.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_bool)
+      )
     ; ( "assume"
       , Symbolic.P.Extern_func.Extern_func
           (Func (Arg (I32, Res), R0), assume_i32) )
diff --git a/test/c/bool.c b/test/c/bool.c
new file mode 100644
index 000000000..57d274bb6
--- /dev/null
+++ b/test/c/bool.c
@@ -0,0 +1,9 @@
+#include <owi.h>
+
+int main() {
+    _Bool b1 = owi_bool(), b2 = owi_bool();
+    owi_assume(b1 || b2);
+    owi_assume(b1 || !b2);
+    owi_assert(b1);
+    return 0;
+}
diff --git a/test/c/bool.t b/test/c/bool.t
new file mode 100644
index 000000000..d8416d82d
--- /dev/null
+++ b/test/c/bool.t
@@ -0,0 +1,2 @@
+  $ owi c ./bool.c
+  All OK
diff --git a/test/c/dune b/test/c/dune
index 15998d46f..b56c172ee 100644
--- a/test/c/dune
+++ b/test/c/dune
@@ -2,7 +2,8 @@
  (deps
   %{bin:owi}
   (package owi)
-  malloc_aligned.c
-  main.c
+  bool.c
+  char.c
   exit.c
-  char.c))
+  main.c
+  malloc_aligned.c))