diff --git a/src/concolic/concolic_wasm_ffi.ml b/src/concolic/concolic_wasm_ffi.ml index b5db968b3..1101e7886 100644 --- a/src/concolic/concolic_wasm_ffi.ml +++ b/src/concolic/concolic_wasm_ffi.ml @@ -41,18 +41,7 @@ module M : in (I32 n, Value.pair n sym_expr) ) - let symbol_char () : Value.int32 Choice.t = - Choice.with_new_symbol (Ty_bitv 32) (fun sym forced_value -> - let n = - match forced_value with - | None -> Int32.logand 0xFFl (Random.bits32 ()) - | Some (Num (I32 n)) -> n - | _ -> assert false - in - let sym_expr = - Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.mk_symbol sym)) - in - (I32 n, Value.pair n sym_expr) ) + let symbol_char = symbol_i8 let symbol_i64 () : Value.int64 Choice.t = Choice.with_new_symbol (Ty_bitv 64) (fun sym forced_value -> diff --git a/src/symbolic/symbolic_wasm_ffi.ml b/src/symbolic/symbolic_wasm_ffi.ml index 75500ec8c..901c70573 100644 --- a/src/symbolic/symbolic_wasm_ffi.ml +++ b/src/symbolic/symbolic_wasm_ffi.ml @@ -35,9 +35,7 @@ module M : Choice.with_new_symbol (Ty_bitv 8) (fun sym -> Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) ) - let symbol_char () = - Choice.with_new_symbol (Ty_bitv 8) (fun sym -> - Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) ) + let symbol_char = symbol_i8 let symbol_i32 () = Choice.with_new_symbol (Ty_bitv 32) Expr.symbol