diff --git a/example/c/README.md b/example/c/README.md
index e2af89b98..7175f9add 100644
--- a/example/c/README.md
+++ b/example/c/README.md
@@ -35,7 +35,7 @@ $ owi c ./poly.c -w1
 ...
 Model:
   (model
-    (symbol_0 (i32 2)))
+    (symbol_0 (i32 4)))
 Reached problem!
 [13]
 ```
@@ -333,9 +333,8 @@ OPTIONS
            skip typechecking pass
 
        -w VAL, --workers=VAL (absent=n)
-           number of workers for symbolic execution. Defaults to a
-           machine-specific value given by the OCaml
-           Domain.recommended_domain_count function.
+           number of workers for symbolic execution. Defaults to the number
+           of physical cores.
 
 COMMON OPTIONS
        --help[=FMT] (default=auto)
diff --git a/example/conc/README.md b/example/conc/README.md
index 65ebc0502..62f8cbd78 100644
--- a/example/conc/README.md
+++ b/example/conc/README.md
@@ -72,9 +72,8 @@ OPTIONS
            skip typechecking pass
 
        -w VAL, --workers=VAL (absent=n)
-           number of workers for symbolic execution. Defaults to a
-           machine-specific value given by the OCaml
-           Domain.recommended_domain_count function.
+           number of workers for symbolic execution. Defaults to the number
+           of physical cores.
 
        --workspace=VAL (absent=owi-out)
            path to the workspace directory
diff --git a/example/sym/README.md b/example/sym/README.md
index 196eefab2..bafaef1fb 100644
--- a/example/sym/README.md
+++ b/example/sym/README.md
@@ -76,9 +76,8 @@ OPTIONS
            skip typechecking pass
 
        -w VAL, --workers=VAL (absent=n)
-           number of workers for symbolic execution. Defaults to a
-           machine-specific value given by the OCaml
-           Domain.recommended_domain_count function.
+           number of workers for symbolic execution. Defaults to the number
+           of physical cores.
 
        --workspace=VAL (absent=owi-out)
            path to the workspace directory
diff --git a/src/ast/types.ml b/src/ast/types.ml
index 8d6c35647..12f1273b1 100644
--- a/src/ast/types.ml
+++ b/src/ast/types.ml
@@ -617,6 +617,71 @@ let rec pp_instr fmt = function
 
 and pp_expr fmt instrs = pp_list ~pp_sep:pp_newline pp_instr fmt instrs
 
+let rec iter_expr f (e : _ expr) = List.iter (iter_instr f) e
+
+and iter_instr f (i : _ instr) =
+  f i;
+  match i with
+  | I32_const _ | I64_const _ | F32_const _ | F64_const _
+  | I_unop (_, _)
+  | F_unop (_, _)
+  | I_binop (_, _)
+  | F_binop (_, _)
+  | I_testop (_, _)
+  | I_relop (_, _)
+  | F_relop (_, _)
+  | I_extend8_s _ | I_extend16_s _ | I64_extend32_s | I32_wrap_i64
+  | I64_extend_i32 _
+  | I_trunc_f (_, _, _)
+  | I_trunc_sat_f (_, _, _)
+  | F32_demote_f64 | F64_promote_f32
+  | F_convert_i (_, _, _)
+  | I_reinterpret_f (_, _)
+  | F_reinterpret_i (_, _)
+  | Ref_null _ | Ref_is_null | Ref_i31 | Ref_func _ | Ref_as_non_null
+  | Ref_cast (_, _)
+  | Ref_test (_, _)
+  | Ref_eq | Drop | Select _ | Local_get _ | Local_set _ | Local_tee _
+  | Global_get _ | Global_set _ | Table_get _ | Table_set _ | Table_size _
+  | Table_grow _ | Table_fill _
+  | Table_copy (_, _)
+  | Table_init (_, _)
+  | Elem_drop _
+  | I_load (_, _)
+  | F_load (_, _)
+  | I_store (_, _)
+  | F_store (_, _)
+  | I_load8 (_, _, _)
+  | I_load16 (_, _, _)
+  | I64_load32 (_, _)
+  | I_store8 (_, _)
+  | I_store16 (_, _)
+  | I64_store32 _ | Memory_size | Memory_grow | Memory_fill | Memory_copy
+  | Memory_init _ | Data_drop _ | Nop | Unreachable | Br _ | Br_if _
+  | Br_table (_, _)
+  | Br_on_cast (_, _, _)
+  | Br_on_cast_fail (_, _, _)
+  | Br_on_non_null _ | Br_on_null _ | Return | Return_call _
+  | Return_call_indirect (_, _)
+  | Return_call_ref _ | Call _
+  | Call_indirect (_, _)
+  | Call_ref _ | Array_get _ | Array_get_u _ | Array_len | Array_new _
+  | Array_new_data (_, _)
+  | Array_new_default _
+  | Array_new_elem (_, _)
+  | Array_new_fixed (_, _)
+  | Array_set _ | I31_get_u | I31_get_s
+  | Struct_get (_, _)
+  | Struct_get_s (_, _)
+  | Struct_new _ | Struct_new_default _
+  | Struct_set (_, _)
+  | Extern_externalize | Extern_internalize ->
+    ()
+  | Block (_, _, e) | Loop (_, _, e) -> iter_expr f e
+  | If_else (_, _, e1, e2) ->
+    iter_expr f e1;
+    iter_expr f e2
+
 (* TODO: func and expr should also be parametrised on block type:
    using (param_type, result_type) M.block_type before simplify and directly an indice after *)
 type 'a func =
diff --git a/src/parser/binary_parser.ml b/src/parser/binary_parser.ml
index 213c4baf6..874e81f52 100644
--- a/src/parser/binary_parser.ml
+++ b/src/parser/binary_parser.ml
@@ -184,12 +184,15 @@ let vector parse_elt input =
 
 let vector_no_id f input = vector (fun _id -> f) input
 
-let check_end_opcode input =
-  let msg = "END opcode expected" in
+let check_end_opcode ?unexpected_eoi_msg input =
+  let msg = Option.value unexpected_eoi_msg ~default:"END opcode expected" in
   match read_byte ~msg input with
   | Ok ('\x0B', input) -> Ok input
   | Ok (c, _input) ->
-    Error (`Msg (Format.sprintf "%s (got %s instead)" msg (Char.escaped c)))
+    Error
+      (`Msg
+        (Format.sprintf "END opcode expected (got %s instead)" (Char.escaped c))
+        )
   | Error _ as e -> e
 
 let check_zero_opcode input =
@@ -331,7 +334,6 @@ let read_block_type types input =
   end
 
 let rec read_instr types input =
-  let old_input = input in
   let* b, input = read_byte ~msg:"read_instr" input in
   match b with
   | '\x00' -> Ok (Unreachable, input)
@@ -627,13 +629,13 @@ let rec read_instr types input =
   | '\xD2' ->
     let+ funcidx, input = read_indice input in
     (Ref_func funcidx, input)
-  | '\xFC' -> read_FC old_input
+  | '\xFC' -> read_FC input
   | c -> Error (`Msg (Format.sprintf "illegal opcode (2) %s" (Char.escaped c)))
 
 and read_expr types input =
   let rec aux acc input =
     match read_byte ~msg:"read_expr" input with
-    | Ok (('\x05' | '\x0b'), _) -> Ok (List.rev acc, input)
+    | Ok (('\x05' | '\x0B'), _) -> Ok (List.rev acc, input)
     | Error _ -> Ok (List.rev acc, input)
     | Ok _ ->
       let* instr, input = read_instr types input in
@@ -675,18 +677,19 @@ let section_parse input ~expected_id default section_content_parse =
   | Some id when id = expected_id ->
     let* () = check_section_id id in
     let* input = Input.sub_suffix 1 input in
+    let* () =
+      if Input.size input = 0 then Error (`Msg "unexpected end") else Ok ()
+    in
     let* size, input = read_U32 input in
     let* () =
-      if size > Input.size input then Error (`Msg "section size mismatch")
+      if size > Input.size input then Error (`Msg "length out of bounds")
       else Ok ()
     in
     let* section_input = Input.sub_prefix size input in
     let* next_input = Input.sub_suffix size input in
     let* res, after_section_input = section_content_parse section_input in
-    if
-      Input.size input - (Input.size next_input + Input.size section_input)
-      <> Input.size after_section_input
-    then Error (`Msg "section size mismatch")
+    if Input.size after_section_input > 0 then
+      Error (`Msg "section size mismatch")
     else Ok (res, next_input)
   | None -> Ok (default, input)
   | Some id ->
@@ -694,6 +697,9 @@ let section_parse input ~expected_id default section_content_parse =
     Ok (default, input)
 
 let parse_utf8_name input =
+  let* () =
+    if Input.size input = 0 then Error (`Msg "unexpected end") else Ok ()
+  in
   let* name, input = read_bytes ~msg:"parse_utf8_name" input in
   let name = string_of_char_list name in
   let+ () = Wutf8.check_utf8 name in
@@ -743,7 +749,7 @@ let read_import input =
   | '\x03' ->
     let+ (mut, val_type), input = read_global_type input in
     ((modul, name, Global (mut, val_type)), input)
-  | _c -> Error (`Msg "SECTION_IMPORT_NO_MATCH")
+  | _c -> Error (`Msg "malformed import kind")
 
 let read_table input =
   let* ref_type, input = read_reftype input in
@@ -855,11 +861,23 @@ let read_locals input =
   (locals, input)
 
 let read_code types input =
-  let* _size, input = read_U32 input in
-  let* locals, input = read_locals input in
-  let* code, input = read_expr types input in
-  let+ input = check_end_opcode input in
-  ((locals, code), input)
+  let* size, input = read_U32 input in
+  let* code_input = Input.sub_prefix size input in
+  let* next_input = Input.sub_suffix size input in
+  let* locals, code_input = read_locals code_input in
+  let* code, code_input = read_expr types code_input in
+  let* () =
+    if Input.size code_input = 0 && Input.size next_input = 0 then
+      Error (`Msg "unexpected end of section or function")
+    else Ok ()
+  in
+  let* code_input =
+    check_end_opcode ~unexpected_eoi_msg:"unexpected end of section or function"
+      code_input
+  in
+  if Input.size code_input > 0 then
+    Error (`Msg "unexpected end of section or function")
+  else Ok ((locals, code), next_input)
 
 (* TODO: merge Elem and Data modes ? *)
 let read_data_active types input =
@@ -1029,12 +1047,20 @@ let sections_iterate (input : Input.t) =
   in
 
   let* () =
-    match data_count_section with
-    | None -> Ok ()
-    | Some len ->
-      if List.compare_length_with data_section len <> 0 then
-        Error (`Msg "data count and data section have inconsistent lengths")
+    match (List.length data_section, data_count_section) with
+    | 0, None -> Ok ()
+    | _data_len, None ->
+      let code_use_dataidx = ref false in
+      let f_iter = function
+        | Data_drop _ | Memory_init _ -> code_use_dataidx := true
+        | _ -> ()
+      in
+      let expr = List.concat_map snd code_section in
+      iter_expr f_iter expr;
+      if !code_use_dataidx then Error (`Msg "data count section required")
       else Ok ()
+    | data_len, Some data_count when data_len = data_count -> Ok ()
+    | _ -> Error (`Msg "data count and data section have inconsistent lengths")
   in
 
   (* Custom *)
diff --git a/src/script/script.ml b/src/script/script.ml
index 9e1f0bc4d..9b4c0e422 100644
--- a/src/script/script.ml
+++ b/src/script/script.ml
@@ -22,6 +22,8 @@ let check_error ~expected ~got : unit Result.t =
        || got = `Msg "constant out of range"
        || got = `Parse_fail "constant out of range" )
        && (expected = "i32 constant out of range" || expected = "i32 constant")
+    || got = `Msg "unexpected end of section or function"
+       && expected = "section size mismatch"
   in
   if not ok then begin
     Error (`Failed_with_but_expected (got, expected))
diff --git a/test/script/reference.t b/test/script/reference.t
index 250ea2503..177759eb7 100644
--- a/test/script/reference.t
+++ b/test/script/reference.t
@@ -4,7 +4,7 @@
   [7]
   $ owi script --no-exhaustion reference/binary-leb128.wast
   $ owi script --no-exhaustion reference/binary.wast
-  expected unexpected end of section or function but got (END opcode expected)
+  expected END opcode expected but got (unexpected end of section or function)
   [51]
   $ owi script --no-exhaustion reference/block.wast
   $ owi script --no-exhaustion reference/br_if.wast
@@ -19,8 +19,6 @@
   $ owi script --no-exhaustion reference/const.wast
   $ owi script --no-exhaustion reference/conversions.wast
   $ owi script --no-exhaustion reference/custom.wast
-  expected unexpected end but got (integer representation too long)
-  [51]
   $ owi script --no-exhaustion reference/data.wast
   $ owi script --no-exhaustion reference/elem.wast
   $ owi script --no-exhaustion reference/endianness.wast
diff --git a/test/script/reference_opt.t b/test/script/reference_opt.t
index fe7391d83..ad79aca6e 100644
--- a/test/script/reference_opt.t
+++ b/test/script/reference_opt.t
@@ -4,7 +4,7 @@
   [7]
   $ owi script --no-exhaustion --optimize reference/binary-leb128.wast
   $ owi script --no-exhaustion --optimize reference/binary.wast
-  expected unexpected end of section or function but got (END opcode expected)
+  expected END opcode expected but got (unexpected end of section or function)
   [51]
   $ owi script --no-exhaustion --optimize reference/block.wast
   $ owi script --no-exhaustion --optimize reference/br_if.wast
@@ -19,8 +19,6 @@
   $ owi script --no-exhaustion --optimize reference/const.wast
   $ owi script --no-exhaustion --optimize reference/conversions.wast
   $ owi script --no-exhaustion --optimize reference/custom.wast
-  expected unexpected end but got (integer representation too long)
-  [51]
   $ owi script --no-exhaustion --optimize reference/data.wast
   $ owi script --no-exhaustion --optimize reference/elem.wast
   $ owi script --no-exhaustion --optimize reference/endianness.wast