diff --git a/CHANGES.md b/CHANGES.md
index 1dfcee3e6..35ecdc3af 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -41,6 +41,7 @@
 - add `owi_label_is_covered` primitive
 - add scopes with `owi_open_scope` and `owi_close_scope` primitives
 - start support for simd instructions
+- add the symbolic execution's entry point to the model
 
 ## 0.2 - 2024-04-24
 
diff --git a/doc/src/symex/quickstart/cpp.md b/doc/src/symex/quickstart/cpp.md
index fce86e683..25cbc895a 100644
--- a/doc/src/symex/quickstart/cpp.md
+++ b/doc/src/symex/quickstart/cpp.md
@@ -24,6 +24,7 @@ owi: [ERROR] Assert failure
 model {
   symbol symbol_0 i32 -2147483648
   symbol symbol_1 i32 -2147483646
+  entry_point main
 }
 owi: [ERROR] Reached problem!
 [13]
diff --git a/doc/src/symex/quickstart/rust.md b/doc/src/symex/quickstart/rust.md
index b0e48cad8..b0e5235a0 100644
--- a/doc/src/symex/quickstart/rust.md
+++ b/doc/src/symex/quickstart/rust.md
@@ -29,6 +29,7 @@ owi: [ERROR] Assert failure
 model {
   symbol symbol_0 i32 -487586839
   symbol symbol_1 i32 486539486
+  entry_point main
 }
 owi: [ERROR] Reached problem!
 [13]
diff --git a/doc/src/symex/quickstart/zig.md b/doc/src/symex/quickstart/zig.md
index 3c4e09b26..1d89f3dca 100644
--- a/doc/src/symex/quickstart/zig.md
+++ b/doc/src/symex/quickstart/zig.md
@@ -35,6 +35,7 @@ $ owi zig ./fib.zig -w1 --no-assert-failure-expression-printing
 owi: [ERROR] Assert failure
 model {
   symbol symbol_0 i32 7
+  entry_point _start
 }
 owi: [ERROR] Reached problem!
 [13]
diff --git a/doc/src/symex/sap/examples.md b/doc/src/symex/sap/examples.md
index ca3c4fae4..f69b87bc0 100644
--- a/doc/src/symex/sap/examples.md
+++ b/doc/src/symex/sap/examples.md
@@ -38,6 +38,7 @@ $ owi c ./poly.c -w1 --no-assert-failure-expression-printing
 owi: [ERROR] Assert failure
 model {
   symbol symbol_0 i32 4
+  entry_point main
 }
 owi: [ERROR] Reached problem!
 [13]
@@ -84,6 +85,7 @@ $ owi c ./poly2.c --no-assert-failure-expression-printing
 owi: [ERROR] Assert failure
 model {
   symbol symbol_0 i32 -2147483644
+  entry_point main
 }
 owi: [ERROR] Reached problem!
 [13]
@@ -135,6 +137,7 @@ $ owi c++ ./poly.cpp -w1 --no-assert-failure-expression-printing
 owi: [ERROR] Assert failure
 model {
   symbol symbol_0 i32 4
+  entry_point main
 }
 owi: [ERROR] Reached problem!
 [13]
@@ -181,6 +184,7 @@ $ owi c++ ./poly2.cpp --no-assert-failure-expression-printing
 owi: [ERROR] Assert failure
 model {
   symbol symbol_0 i32 -2147483644
+  entry_point main
 }
 owi: [ERROR] Reached problem!
 [13]
@@ -305,6 +309,7 @@ model {
   symbol symbol_25 i32
   symbol symbol_26 i32
   symbol symbol_27 i32
+  entry_point main
 }
 owi: [ERROR] Reached problem!
 [13]
@@ -371,6 +376,7 @@ model {
   symbol symbol_4 i32
   symbol symbol_5 i32
   symbol symbol_6 i32
+  entry_point main
 }
 owi: [ERROR] Reached problem!
 [13]
diff --git a/doc/src/symex/verification/eacsl.md b/doc/src/symex/verification/eacsl.md
index 187c31f9e..66c94f4d5 100644
--- a/doc/src/symex/verification/eacsl.md
+++ b/doc/src/symex/verification/eacsl.md
@@ -97,6 +97,7 @@ $ owi c --e-acsl primes.c -w1
 owi: [ERROR] Assert failure: false
 model {
   symbol symbol_0 i32 2
+  entry_point main
 }
 owi: [ERROR] Reached problem!
 [13]
diff --git a/src/cmd/cmd_iso.ml b/src/cmd/cmd_iso.ml
index e1fcfebe6..d4a092d06 100644
--- a/src/cmd/cmd_iso.ml
+++ b/src/cmd/cmd_iso.ml
@@ -443,5 +443,5 @@ let cmd ~deterministic_result_order ~fail_mode ~files ~model_format
       Cmd_sym.handle_result ~fail_mode ~workers ~solver
         ~deterministic_result_order ~model_format ~no_value
         ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure
-        ~model_out_file ~with_breadcrumbs result )
+        ~model_out_file ~with_breadcrumbs ~entry_point:None result )
     () common_exports
diff --git a/src/cmd/cmd_replay.ml b/src/cmd/cmd_replay.ml
index 6736efbd7..6936dc4e2 100644
--- a/src/cmd/cmd_replay.ml
+++ b/src/cmd/cmd_replay.ml
@@ -261,19 +261,19 @@ let run_file ~unsafe ~optimize ~entry_point ~invoke_with_symbols filename model
 
 let cmd ~unsafe ~optimize ~replay_file ~source_file ~entry_point
   ~invoke_with_symbols =
+  let file_ext = Fpath.get_ext replay_file in
   let* parse_fn =
-    let ext = Fpath.get_ext replay_file in
-    match String.lowercase_ascii ext with
+    match String.lowercase_ascii file_ext with
     | ".json" -> Ok Symbol_scope.model_of_json
     | ".scfg" -> Ok Symbol_scope.model_of_scfg
-    | _ -> Error (`Unsupported_file_extension ext)
+    | _ -> Error (`Unsupported_file_extension file_ext)
   in
   let* file_content = Bos.OS.File.read replay_file in
-  let* model =
+  let* model_entry_point, model =
     match parse_fn file_content with
     | Error (`Msg msg) -> Error (`Invalid_model msg)
     | Error err -> Error err
-    | Ok model ->
+    | Ok (entry_point, model) ->
       let bindings = Smtml.Model.get_bindings model in
       let+ model =
         list_map
@@ -298,8 +298,16 @@ let cmd ~unsafe ~optimize ~replay_file ~source_file ~entry_point
                    (Fmt.str "unexpected value type: %a" Smtml.Value.pp v) ) )
           bindings
       in
-      Array.of_list model
+      (entry_point, Array.of_list model)
   in
+  let entry_point =
+    if Option.is_none entry_point then model_entry_point else entry_point
+  in
+  Logs.debug (fun m ->
+    m "Specified entry point: %s" (Option.value ~default:"None" entry_point) );
+  Logs.debug (fun m ->
+    m "Entry point inside model: %s"
+      (Option.value ~default:"None" model_entry_point) );
   let+ () =
     run_file ~unsafe ~optimize ~entry_point ~invoke_with_symbols source_file
       model
diff --git a/src/cmd/cmd_sym.ml b/src/cmd/cmd_sym.ml
index 48eca3bb5..22d7e8453 100644
--- a/src/cmd/cmd_sym.ml
+++ b/src/cmd/cmd_sym.ml
@@ -34,7 +34,7 @@ let run_file ~entry_point ~unsafe ~rac ~srac ~optimize ~invoke_with_symbols _pc
   Interpret.Symbolic.modul link_state.envs m
 
 let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure
-  ~no_assert_failure_expression_printing ~with_breadcrumbs bug =
+  ~no_assert_failure_expression_printing ~with_breadcrumbs ~entry_point bug =
   let pp fmt (model, labels, breadcrumbs, scoped_values) =
     match model_format with
     | Cmd_utils.Json ->
@@ -62,7 +62,8 @@ let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure
             } )
           labels
       in
-      let children =
+      let model = { model with children = model.children @ lbls } in
+      let model =
         if with_breadcrumbs then
           let bcrumbs =
             [ { Scfg.Types.name = "breadcrumbs"
@@ -71,10 +72,23 @@ let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure
               }
             ]
           in
-          model.children @ lbls @ bcrumbs
-        else model.children @ lbls
+          { model with children = model.children @ bcrumbs }
+        else model
       in
-      Scfg.Pp.directive fmt { model with children }
+      let model =
+        match entry_point with
+        | Some entry_point ->
+          let ep =
+            [ { Scfg.Types.name = "entry_point"
+              ; params = [ entry_point ]
+              ; children = []
+              }
+            ]
+          in
+          { model with children = model.children @ ep }
+        | None -> model
+      in
+      Scfg.Pp.directive fmt model
   in
   let to_file path model labels breadcrumbs symbol_scopes =
     let model_ext = match model_format with Json -> "json" | Scfg -> "scfg" in
@@ -117,7 +131,7 @@ let print_bug ~model_format ~model_out_file ~id ~no_value ~no_stop_at_failure
 
 let print_and_count_failures ~model_format ~model_out_file ~no_value
   ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure
-  ~count_acc ~results ~with_breadcrumbs =
+  ~count_acc ~results ~with_breadcrumbs ~entry_point =
   let test_suite_dir = Fpath.(workspace / "test-suite") in
   let* (_created : bool) =
     if not no_value then OS.Dir.create test_suite_dir else Ok false
@@ -133,7 +147,7 @@ let print_and_count_failures ~model_format ~model_out_file ~no_value
           let* () =
             print_bug ~model_format ~model_out_file ~id:count_acc ~no_value
               ~no_stop_at_failure ~no_assert_failure_expression_printing
-              ~with_breadcrumbs bug
+              ~with_breadcrumbs ~entry_point bug
           in
           Ok model
         | `Error e -> Error e
@@ -162,7 +176,7 @@ let sort_results deterministic_result_order results =
 let handle_result ~workers ~no_stop_at_failure ~no_value
   ~no_assert_failure_expression_printing ~deterministic_result_order ~fail_mode
   ~workspace ~solver ~model_format ~model_out_file ~with_breadcrumbs
-  (result : unit Symbolic.Choice.t) =
+  ~entry_point (result : unit Symbolic.Choice.t) =
   let thread = Thread_with_memory.init () in
   let res_queue = Wq.make () in
   let path_count = Atomic.make 0 in
@@ -196,7 +210,7 @@ let handle_result ~workers ~no_stop_at_failure ~no_value
   let* count =
     print_and_count_failures ~model_format ~model_out_file ~no_value
       ~no_assert_failure_expression_printing ~workspace ~no_stop_at_failure
-      ~count_acc:0 ~results ~with_breadcrumbs
+      ~count_acc:0 ~results ~with_breadcrumbs ~entry_point
   in
   Logs.info (fun m -> m "Completed paths: %d" (Atomic.get path_count));
   let+ () = if count > 0 then Error (`Found_bug count) else Ok () in
@@ -226,4 +240,4 @@ let cmd ~unsafe ~rac ~srac ~optimize ~workers ~no_stop_at_failure ~no_value
   in
   handle_result ~fail_mode ~workers ~solver ~deterministic_result_order
     ~model_format ~no_value ~no_assert_failure_expression_printing ~workspace
-    ~no_stop_at_failure ~model_out_file ~with_breadcrumbs result
+    ~no_stop_at_failure ~model_out_file ~with_breadcrumbs ~entry_point result
diff --git a/src/cmd/cmd_sym.mli b/src/cmd/cmd_sym.mli
index 139bb5445..835ddd7fe 100644
--- a/src/cmd/cmd_sym.mli
+++ b/src/cmd/cmd_sym.mli
@@ -23,6 +23,7 @@ val handle_result :
   -> model_format:Cmd_utils.model_format
   -> model_out_file:Fpath.t option
   -> with_breadcrumbs:bool
+  -> entry_point:string option
   -> unit Symbolic.Choice.t
   -> unit Result.t
 
diff --git a/src/symbolic/symbol_scope.ml b/src/symbolic/symbol_scope.ml
index 18985b086..475ba471d 100644
--- a/src/symbolic/symbol_scope.ml
+++ b/src/symbolic/symbol_scope.ml
@@ -204,7 +204,10 @@ let model_of_json json_str =
     match List.assoc_opt "model" root with
     | Some items ->
       let+ () = process_json (Util.to_list items) in
-      tbl
+      let entry_point =
+        Option.map Util.to_string (List.assoc_opt "entry_point" root)
+      in
+      (entry_point, tbl)
     | None -> Fmt.error_msg "JSON does not contain model field" )
   | _ ->
     Fmt.error_msg "Invalid JSON format for symbol scope:@. %a"
@@ -238,6 +241,10 @@ let model_of_scfg scfg =
   match Query.get_dir "model" scfg with
   | Some model ->
     let+ () = process_dirs model.children in
-    tbl
+    let entry_point =
+      let dir = Query.get_dir "entry_point" model.children in
+      Option.bind dir (fun dir -> Result.to_option @@ Query.get_param 0 dir)
+    in
+    (entry_point, tbl)
   | None ->
     Fmt.error_msg "Could not find the directive `model` in the scfg config"
diff --git a/src/symbolic/symbol_scope.mli b/src/symbolic/symbol_scope.mli
index c0a2c21f5..afcb27c72 100644
--- a/src/symbolic/symbol_scope.mli
+++ b/src/symbolic/symbol_scope.mli
@@ -24,6 +24,6 @@ val to_json :
   -> t
   -> [> `Assoc of (string * Yojson.Basic.t) list ]
 
-val model_of_json : string -> Smtml.Model.t Result.t
+val model_of_json : string -> (string option * Smtml.Model.t) Result.t
 
-val model_of_scfg : string -> Smtml.Model.t Result.t
+val model_of_scfg : string -> (string option * Smtml.Model.t) Result.t
diff --git a/test/c/collections-c/tests_array.t b/test/c/collections-c/tests_array.t
index 369ab2995..38a91c998 100644
--- a/test/c/collections-c/tests_array.t
+++ b/test/c/collections-c/tests_array.t
@@ -73,6 +73,7 @@ Array tests:
     symbol symbol_1 i32 0
     symbol symbol_2 i32 0
     symbol symbol_3 i32 0
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   
diff --git a/test/c/collections-c/tests_buggy.t b/test/c/collections-c/tests_buggy.t
index d227ab51e..acc8caa3f 100644
--- a/test/c/collections-c/tests_buggy.t
+++ b/test/c/collections-c/tests_buggy.t
@@ -4,6 +4,7 @@ Bug-triggering tests:
   owi: [ERROR] Trap: memory heap buffer overflow
   model {
     symbol symbol_0 i32 8
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
@@ -22,6 +23,7 @@ Bug-triggering tests:
     symbol symbol_8 i32
     symbol symbol_9 i32
     symbol symbol_10 i32
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/collections-c/tests_pqueue.t b/test/c/collections-c/tests_pqueue.t
index 3ba611242..ccfff8a77 100644
--- a/test/c/collections-c/tests_pqueue.t
+++ b/test/c/collections-c/tests_pqueue.t
@@ -10,6 +10,7 @@ Pqueue tests:
     symbol symbol_3 i32
     symbol symbol_4 i32
     symbol symbol_5 i32
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   
@@ -29,6 +30,7 @@ Pqueue tests:
     symbol symbol_6 i32
     symbol symbol_7 i32
     symbol symbol_8 i32
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   
diff --git a/test/c/double_free.t b/test/c/double_free.t
index 0ec0dc759..00621fe7d 100644
--- a/test/c/double_free.t
+++ b/test/c/double_free.t
@@ -1,5 +1,7 @@
   $ owi c double_free.c --entry-point=f
   owi: [ERROR] Trap: double free
-  model
+  model {
+    entry_point f
+  }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/dune b/test/c/dune
index 4efc03a53..9cdf4d354 100644
--- a/test/c/dune
+++ b/test/c/dune
@@ -15,6 +15,7 @@
   main.c
   malloc_aligned.c
   malloc_zero.c
+  model_with_entry_point.c
   multi_model.c
   range.c
   scopes.c))
diff --git a/test/c/eacsl/function/integer_dividable.t b/test/c/eacsl/function/integer_dividable.t
index b27d2253b..bd9fb2451 100644
--- a/test/c/eacsl/function/integer_dividable.t
+++ b/test/c/eacsl/function/integer_dividable.t
@@ -3,6 +3,7 @@
   model {
     symbol symbol_0 i32
     symbol symbol_1 i32
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/eacsl/function/max.t b/test/c/eacsl/function/max.t
index 8c04ea8c8..f53e8a05b 100644
--- a/test/c/eacsl/function/max.t
+++ b/test/c/eacsl/function/max.t
@@ -3,6 +3,7 @@
   model {
     symbol symbol_0 i32
     symbol symbol_1 i32
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/eacsl/function/max_ptr.t b/test/c/eacsl/function/max_ptr.t
index ab1a66d01..1da990fec 100644
--- a/test/c/eacsl/function/max_ptr.t
+++ b/test/c/eacsl/function/max_ptr.t
@@ -3,6 +3,7 @@
   model {
     symbol symbol_0 i32
     symbol symbol_1 i32
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/eacsl/ghost/case.t b/test/c/eacsl/ghost/case.t
index a9aff9ee7..f6db0bc19 100644
--- a/test/c/eacsl/ghost/case.t
+++ b/test/c/eacsl/ghost/case.t
@@ -2,6 +2,7 @@
   owi: [ERROR] Assert failure: (bool.ne symbol_0 2)
   model {
     symbol symbol_0 i32 2
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/eacsl/ghost/default.t b/test/c/eacsl/ghost/default.t
index 6764e6426..61bb8add4 100644
--- a/test/c/eacsl/ghost/default.t
+++ b/test/c/eacsl/ghost/default.t
@@ -2,6 +2,7 @@
   owi: [ERROR] Assert failure: (i32.lt_u symbol_0 2)
   model {
     symbol symbol_0 i32
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/eacsl/ghost/else.t b/test/c/eacsl/ghost/else.t
index abf66ad27..40f735a58 100644
--- a/test/c/eacsl/ghost/else.t
+++ b/test/c/eacsl/ghost/else.t
@@ -2,6 +2,7 @@
   owi: [ERROR] Assert failure
   model {
     symbol symbol_0 i32
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/eacsl/ghost/global.t b/test/c/eacsl/ghost/global.t
index 2d6d10115..445c7d485 100644
--- a/test/c/eacsl/ghost/global.t
+++ b/test/c/eacsl/ghost/global.t
@@ -2,6 +2,7 @@
   owi: [ERROR] Assert failure: (i32.lt_s symbol_0 20)
   model {
     symbol symbol_0 i32 20
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/entry_point.t b/test/c/entry_point.t
index e14805edf..f58c0b4c6 100644
--- a/test/c/entry_point.t
+++ b/test/c/entry_point.t
@@ -3,6 +3,7 @@ entry_point:
   owi: [ERROR] Assert failure: (i32.lt_s symbol_0 19)
   model {
     symbol symbol_0 i32 19
+    entry_point fun
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/exit.t b/test/c/exit.t
index 4a1870524..96dc358bd 100644
--- a/test/c/exit.t
+++ b/test/c/exit.t
@@ -2,6 +2,7 @@
   owi: [ERROR] Assert failure: (i32.to_bool symbol_0)
   model {
     symbol symbol_0 i32
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/invisible_bool.t b/test/c/invisible_bool.t
index 398a95d84..63298d086 100644
--- a/test/c/invisible_bool.t
+++ b/test/c/invisible_bool.t
@@ -2,6 +2,7 @@
   owi: [ERROR] Assert failure: false
   model {
     symbol symbol_0 i1
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/invoke_with_symbols.t b/test/c/invoke_with_symbols.t
index 903842498..d06542a84 100644
--- a/test/c/invoke_with_symbols.t
+++ b/test/c/invoke_with_symbols.t
@@ -1,10 +1,14 @@
-  $ owi c --entry-point=f --invoke-with-symbols ./invoke_with_symbols.c
-  owi: [ERROR] Assert failure: (f32.ne (f32.convert_i32_s symbol_0) symbol_2)
+  $ owi c -O0 --entry-point=f --invoke-with-symbols ./invoke_with_symbols.c
+  owi: [ERROR] Assert failure: (f32.ne
+                                (f32.reinterpret_int
+                                 (i32.reinterpret_float symbol_2))
+                                (f32.convert_i32_s symbol_0))
   model {
     symbol symbol_0 i32 1
     symbol symbol_1 i64 0
     symbol symbol_2 f32 1.
     symbol symbol_3 f64 -1234.
+    entry_point f
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/label.t b/test/c/label.t
index ee4cf0dc4..bc9bbbebc 100644
--- a/test/c/label.t
+++ b/test/c/label.t
@@ -3,11 +3,13 @@
   model {
     symbol symbol_0 i32 50
     label 1 label_1
+    entry_point main
   }
   owi: [ERROR] Assert failure: false
   model {
     symbol symbol_0 i32 49
     label 2 label_2
+    entry_point main
   }
   owi: [ERROR] Reached 2 problems!
   [13]
diff --git a/test/c/main.t b/test/c/main.t
index 89f22a22b..b5b0328c6 100644
--- a/test/c/main.t
+++ b/test/c/main.t
@@ -7,6 +7,7 @@
     symbol symbol_3 i8
     symbol symbol_4 i8
     symbol symbol_5 i8
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/malloc_zero.t b/test/c/malloc_zero.t
index 2e543bf8b..ea4a59882 100644
--- a/test/c/malloc_zero.t
+++ b/test/c/malloc_zero.t
@@ -1,13 +1,17 @@
   $ owi c ./malloc_zero.c --entry-point=f1 -w1 -O0
   owi: [ERROR] Assert failure: false
-  model
+  model {
+    entry_point f1
+  }
   owi: [ERROR] Reached problem!
   [13]
   $ owi c ./malloc_zero.c --entry-point=f2 -w1 -O0
   All OK!
   $ owi c ./malloc_zero.c --entry-point=g1 -w1 -O0
   owi: [ERROR] Assert failure: false
-  model
+  model {
+    entry_point g1
+  }
   owi: [ERROR] Reached problem!
   [13]
   $ owi c ./malloc_zero.c --entry-point=g2 -w1 -O0
diff --git a/test/c/model_with_entry_point.c b/test/c/model_with_entry_point.c
new file mode 100644
index 000000000..9a4cad08b
--- /dev/null
+++ b/test/c/model_with_entry_point.c
@@ -0,0 +1,17 @@
+#include <owi.h>
+
+int fun() {
+  int i = owi_i32();
+  owi_assume(i < 2);
+  owi_assume(i > 0);
+  owi_assert(i == 2);
+  return i;
+}
+
+int main() {
+  int i = owi_i32();
+  owi_assume(i < 3);
+  owi_assume(i > 1);
+  owi_assert(i == 3);
+  return i;
+}
diff --git a/test/c/model_with_entry_point.t b/test/c/model_with_entry_point.t
new file mode 100644
index 000000000..75bcd3c8d
--- /dev/null
+++ b/test/c/model_with_entry_point.t
@@ -0,0 +1,25 @@
+  $ owi c model_with_entry_point.c -O0 --entry-point=main
+  owi: [ERROR] Assert failure: (bool.eq symbol_0 3)
+  model {
+    symbol symbol_0 i32 2
+    entry_point main
+  }
+  owi: [ERROR] Reached problem!
+  [13]
+
+  $ owi c model_with_entry_point.c -O0 --entry-point=fun
+  owi: [ERROR] Assert failure: (bool.eq symbol_0 2)
+  model {
+    symbol symbol_0 i32 1
+    entry_point fun
+  }
+  owi: [ERROR] Reached problem!
+  [13]
+
+  $ owi c model_with_entry_point.c -O0 --entry-point=fun --model-out-file=output.scfg -o output.wasm
+  owi: [ERROR] Assert failure: (bool.eq symbol_0 2)
+  owi: [ERROR] Reached problem!
+  [13]
+
+  $ owi replay output.wasm --replay-file=output.scfg
+  Assertion failure was correctly reached!
diff --git a/test/c/range.t b/test/c/range.t
index 34738fb03..3a21e12fd 100644
--- a/test/c/range.t
+++ b/test/c/range.t
@@ -3,6 +3,7 @@
   model {
     symbol symbol_0 i32 16
     symbol symbol_1 i32 100
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/scopes.t b/test/c/scopes.t
index 7eba0d25d..5b118df7f 100644
--- a/test/c/scopes.t
+++ b/test/c/scopes.t
@@ -17,6 +17,7 @@
     }
     symbol symbol_8 i32 aaa
     symbol symbol_9 i32 aaa
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/c/test-comp/simple.t b/test/c/test-comp/simple.t
index a92d6d6a4..e033669e8 100644
--- a/test/c/test-comp/simple.t
+++ b/test/c/test-comp/simple.t
@@ -2,6 +2,7 @@
   owi: [ERROR] Assert failure: (bool.ne (i32.mul symbol_0 symbol_0) 0)
   model {
     symbol symbol_0 i32 0
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/cpp/entry_point.t b/test/cpp/entry_point.t
index c5faf1a9d..f46f6a490 100644
--- a/test/cpp/entry_point.t
+++ b/test/cpp/entry_point.t
@@ -3,6 +3,7 @@ entry_point:
   owi: [ERROR] Assert failure: (i32.lt_s symbol_0 19)
   model {
     symbol symbol_0 i32 19
+    entry_point fun
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/replay/alloc.t b/test/replay/alloc.t
index 0b19e39b2..69eba480a 100644
--- a/test/replay/alloc.t
+++ b/test/replay/alloc.t
@@ -2,6 +2,7 @@
   owi: [ERROR] Assert failure: false
   model {
     symbol symbol_0 i32
+    entry_point main
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/rust/entry_point.t b/test/rust/entry_point.t
index 3943f0a98..9d65c48ec 100644
--- a/test/rust/entry_point.t
+++ b/test/rust/entry_point.t
@@ -3,6 +3,7 @@ entry_point:
   owi: [ERROR] Assert failure: (i32.le_s 4 symbol_0)
   model {
     symbol symbol_0 i32 2
+    entry_point fun
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/sym/entry_points/export.t b/test/sym/entry_points/export.t
index 2b5c6259c..848f23c17 100644
--- a/test/sym/entry_points/export.t
+++ b/test/sym/entry_points/export.t
@@ -10,6 +10,7 @@ export:
   owi: [ERROR] Assert failure: (i32.lt_u symbol_0 19)
   model {
     symbol symbol_0 i32 19
+    entry_point fun
   }
   owi: [ERROR] Reached problem!
   [13]
diff --git a/test/sym/print_pc.t b/test/sym/print_pc.t
index 0648d26bc..767ffb057 100644
--- a/test/sym/print_pc.t
+++ b/test/sym/print_pc.t
@@ -115,5 +115,6 @@
   owi: [DEBUG] Current scope tokens: [symbol symbol_0]
   model {
     symbol symbol_0 i32 0
+    entry_point f
   }
   owi: [ERROR] Reached problem!
diff --git a/test/zig/entry_point.t b/test/zig/entry_point.t
index ca4a58a91..13bd51960 100644
--- a/test/zig/entry_point.t
+++ b/test/zig/entry_point.t
@@ -3,6 +3,7 @@ entry_point:
   owi: [ERROR] Assert failure: (i32.le_s 5 symbol_0)
   model {
     symbol symbol_0 i32 4
+    entry_point fun
   }
   owi: [ERROR] Reached problem!
   [13]