diff --git a/.gitmodules b/.gitmodules
index b2d9465a..f65d406b 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -14,3 +14,6 @@
 	path = test/c/collections-c/files
 	url = https://github.com/zapashcanon/Collections-C.git
 	shallow = true
+[submodule "bench/symbiotic"]
+	path = bench/symbiotic
+	url = https://github.com/filipeom/symbiotic-testcomp.git
diff --git a/bench/dune b/bench/dune
index 9827c0ce..64e51103 100644
--- a/bench/dune
+++ b/bench/dune
@@ -1 +1 @@
-(dirs :standard \ klee pie results-*)
+(dirs :standard \ klee symbiotic pie results-*)
diff --git a/bench/symbiotic b/bench/symbiotic
new file mode 160000
index 00000000..787214a3
--- /dev/null
+++ b/bench/symbiotic
@@ -0,0 +1 @@
+Subproject commit 787214a32bb75a663b63a5e95a665f8e55847e78
diff --git a/bench/tool/tool.ml b/bench/tool/tool.ml
index f51e5891..74b29f00 100644
--- a/bench/tool/tool.ml
+++ b/bench/tool/tool.ml
@@ -8,10 +8,14 @@ type t =
       ; solver : S.solver_type
       }
   | Klee
+  | Symbiotic
 
 let ( let+ ) o f = match o with Ok v -> Ok (f v) | Error _ as e -> e
 
-let to_short_name = function Owi _ -> "owi" | Klee -> "klee"
+let to_short_name = function
+  | Owi _ -> "owi"
+  | Klee -> "klee"
+  | Symbiotic -> "symbiotic"
 
 let to_reference_name = function
   | Owi { concolic; workers; optimisation_level; solver } ->
@@ -19,12 +23,15 @@ let to_reference_name = function
       S.pp_solver_type solver
       (if concolic then "_concolic" else "")
   | Klee -> "klee"
+  | Symbiotic -> "symbiotic"
 
 let mk_owi ~concolic ~workers ~optimisation_level ~solver =
   Owi { concolic; workers; optimisation_level; solver }
 
 let mk_klee () = Klee
 
+let mk_symbiotic () = Symbiotic
+
 exception Sigchld
 
 let wait_pid =
@@ -96,6 +103,17 @@ let wait_pid =
             if !has_found_error then Reached rusage else Nothing rusage
           end
           else Other (rusage, code)
+        | Symbiotic ->
+          if code = 0 then begin
+            match Bos.OS.File.read dst_stderr with
+            | Error (`Msg err) -> failwith err
+            | Ok data -> (
+              let error = Astring.String.find_sub ~sub:"Found ERROR!" data in
+              match error with
+              | Some _ -> Reached rusage
+              | None -> Nothing rusage )
+          end
+          else Other (rusage, code)
       end
       | WSIGNALED n -> Signaled (rusage, n)
       | WSTOPPED n -> Stopped (rusage, n)
@@ -131,6 +149,15 @@ let execvp ~output_dir tool file timeout =
         ; timeout
         ; file
         ] )
+    | Symbiotic ->
+      let path_to_symbiotic = "symbiotic/bin/symbiotic" in
+      ( path_to_symbiotic
+      , [ path_to_symbiotic
+        ; "--test-comp"
+        ; Format.sprintf "--timeout=%s" timeout
+        ; "--prp=testcomp/sv-benchmarks/c/properties/coverage-error-call.prp"
+        ; file
+        ] )
   in
   let args = Array.of_list args in
   Unix.execvp bin args
diff --git a/bench/tool/tool.mli b/bench/tool/tool.mli
index 3d63bce6..2cf1097f 100644
--- a/bench/tool/tool.mli
+++ b/bench/tool/tool.mli
@@ -13,6 +13,8 @@ val mk_owi :
 
 val mk_klee : unit -> t
 
+val mk_symbiotic : unit -> t
+
 val fork_and_run_on_file :
      i:int
   -> fmt:Format.formatter