diff options
Diffstat (limited to 'src/lem_interp/interp_inter_imp.lem')
| -rw-r--r-- | src/lem_interp/interp_inter_imp.lem | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/lem_interp/interp_inter_imp.lem b/src/lem_interp/interp_inter_imp.lem index 690f8bcf..da87842d 100644 --- a/src/lem_interp/interp_inter_imp.lem +++ b/src/lem_interp/interp_inter_imp.lem @@ -437,7 +437,7 @@ let rec interp_to_outcome mode context thunk = length tracking value v_tracking (fun b -> match return with - | Nothing -> (IState next_state context) + | Nothing -> (IState (Interp.add_answer_to_stack next_state Interp.unitv) context) | Just return_bool -> return_bool (IState next_state context) b end) else Error "Memory address on write is not 64 bits" | _ -> Error ("Memory " ^ i ^ " function with write kind not found") |