diff --git a/infer/src/pulse/Pulse.ml b/infer/src/pulse/Pulse.ml
index 7d32152b3..084929e3c 100644
--- a/infer/src/pulse/Pulse.ml
+++ b/infer/src/pulse/Pulse.ml
@@ -8,10 +8,10 @@
 open! IStd
 module F = Format
 module L = Logging
-open IResult.Let_syntax
 module IRAttributes = Attributes
 open PulseBasicInterface
 open PulseDomainInterface
+open PulseOperations.Import
 
 let exec_list_of_list_result = function
   | Ok posts ->
@@ -24,17 +24,27 @@ let exec_list_of_list_result = function
 
 let report_on_error {InterproceduralAnalysis.proc_desc; tenv; err_log} result =
   PulseReport.report_error proc_desc tenv err_log result
-  >>| List.map ~f:(fun post -> ExecutionDomain.ContinueProgram post)
+  >>| List.map ~f:(fun post -> ContinueProgram post)
   |> exec_list_of_list_result
 
 
-let report_on_error_list {InterproceduralAnalysis.proc_desc; tenv; err_log} result =
-  PulseReport.report_error proc_desc tenv err_log result |> exec_list_of_list_result
+let post_of_report_result = function
+  | Ok post ->
+      Some post
+  | Error Unsat ->
+      None
+  | Error (Sat post) ->
+      Some post
+
+
+let report_on_error_list {InterproceduralAnalysis.proc_desc; tenv; err_log} results =
+  List.filter_map results ~f:(fun exec_result ->
+      PulseReport.report_error proc_desc tenv err_log exec_result |> post_of_report_result )
 
 
 let report_topl_errors proc_desc err_log summary =
   let f = function
-    | ExecutionDomain.ContinueProgram astate ->
+    | ContinueProgram astate ->
         PulseTopl.report_errors proc_desc err_log (AbductiveDomain.Topl.get astate)
     | _ ->
         ()
@@ -60,24 +70,24 @@ module PulseTransferFunctions = struct
     AnalysisCallbacks.proc_resolve_attributes pname |> Option.map ~f:ProcAttributes.get_pvar_formals
 
 
-  let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc; tenv; err_log}
-      ret callee_pname call_exp actuals call_loc astate =
+  let interprocedural_call {InterproceduralAnalysis.analyze_dependency; proc_desc} ret callee_pname
+      call_exp actuals call_loc astate =
     match callee_pname with
     | Some callee_pname when not Config.pulse_intraprocedural_only ->
         let formals_opt = get_pvar_formals callee_pname in
         let callee_data = analyze_dependency callee_pname in
-        PulseOperations.call ~caller_proc_desc:proc_desc tenv err_log ~callee_data call_loc
-          callee_pname ~ret ~actuals ~formals_opt astate
+        PulseOperations.call ~caller_proc_desc:proc_desc ~callee_data call_loc callee_pname ~ret
+          ~actuals ~formals_opt astate
     | _ ->
         L.d_printfln "Skipping indirect call %a@\n" Exp.pp call_exp ;
         let astate =
           let arg_values = List.map actuals ~f:(fun ((value, _), _) -> value) in
           PulseOperations.conservatively_initialize_args arg_values astate
         in
-        Ok
-          [ Domain.ContinueProgram
-              (PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals
-                 ~formals_opt:None astate) ]
+        [ Ok
+            (ContinueProgram
+               (PulseOperations.unknown_call call_loc (SkippedUnknownCall call_exp) ~ret ~actuals
+                  ~formals_opt:None astate)) ]
 
 
   (** has an object just gone out of scope? *)
@@ -126,7 +136,7 @@ module PulseTransferFunctions = struct
       | ISLLatentMemoryError _ | AbortProgram _ | LatentAbortProgram _ | ExitProgram _ ->
           exec_state
     in
-    Result.map ~f:(List.map ~f:do_one_exec_state) exec_state_res
+    List.map ~f:(Result.map ~f:do_one_exec_state) exec_state_res
 
 
   let topl_store_step loc ~lhs ~rhs:_ astate =
@@ -145,7 +155,7 @@ module PulseTransferFunctions = struct
   let dispatch_call ({InterproceduralAnalysis.proc_desc; tenv} as analysis_data) ret call_exp
       actuals call_loc flags astate =
     (* evaluate all actuals *)
-    let* astate, rev_func_args =
+    let<*> astate, rev_func_args =
       List.fold_result actuals ~init:(astate, [])
         ~f:(fun (astate, rev_func_args) (actual_exp, actual_typ) ->
           let+ astate, actual_evaled = PulseOperations.eval Read call_loc actual_exp astate in
@@ -166,7 +176,7 @@ module PulseTransferFunctions = struct
           None
     in
     (* do interprocedural call then destroy objects going out of scope *)
-    let exec_state_res =
+    let exec_states_res =
       match model with
       | Some (model, callee_procname) ->
           L.d_printfln "Found model for call@\n" ;
@@ -191,29 +201,33 @@ module PulseTransferFunctions = struct
           PerfEvent.(log (fun logger -> log_end_event logger ())) ;
           r
     in
-    let exec_state_res =
+    let exec_states_res =
       if Topl.is_deep_active () then
         match callee_pname with
         | Some callee_pname ->
-            topl_small_step call_loc callee_pname func_args ret exec_state_res
+            topl_small_step call_loc callee_pname func_args ret exec_states_res
         | None ->
-            (* skip, as above for non-topl *) exec_state_res
-      else exec_state_res
+            (* skip, as above for non-topl *) exec_states_res
+      else exec_states_res
     in
-    let+ exec_state =
+    let exec_states_res =
       match get_out_of_scope_object callee_pname actuals flags with
       | Some pvar_typ ->
           L.d_printfln "%a is going out of scope" Pvar.pp_value (fst pvar_typ) ;
-          let* exec_states = exec_state_res in
-          List.map exec_states ~f:(fun exec_state ->
-              exec_object_out_of_scope call_loc pvar_typ exec_state )
-          |> Result.all
+          List.map exec_states_res ~f:(fun exec_state ->
+              exec_state >>= exec_object_out_of_scope call_loc pvar_typ )
       | None ->
-          exec_state_res
+          exec_states_res
     in
     if Option.exists callee_pname ~f:IRAttributes.is_no_return then
-      ExecutionDomain.force_exit_program proc_desc exec_state
-    else exec_state
+      List.filter_map exec_states_res ~f:(fun exec_state_res ->
+          match exec_state_res with
+          | Error _ as err ->
+              Some err
+          | Ok exec_state ->
+              ExecutionDomain.force_exit_program proc_desc exec_state
+              |> Option.map ~f:(fun exec_state -> Ok exec_state) )
+    else exec_states_res
 
 
   (* [get_dealloc_from_dynamic_types vars_types loc] returns a dealloc procname and vars and
@@ -271,7 +285,7 @@ module PulseTransferFunctions = struct
     L.d_printfln ~color:Pp.Orange
       "Executing injected call to dealloc for vars (%a) that are exiting the scope@."
       (Pp.seq ~sep:"," Var.pp) vars ;
-    let astates = List.fold ~f:call_dealloc dealloc_data ~init:[Domain.ContinueProgram astate] in
+    let astates = List.fold ~f:call_dealloc dealloc_data ~init:[ContinueProgram astate] in
     (astates, ret_vars)
 
 
@@ -362,13 +376,13 @@ module PulseTransferFunctions = struct
           in
           report_on_error analysis_data result
       | Prune (condition, loc, _is_then_branch, _if_kind) ->
-          (let+ astate = PulseOperations.prune loc ~condition astate in
+          (let<*> astate = PulseOperations.prune loc ~condition astate in
            if PulseArithmetic.is_unsat_cheap astate then
              (* [condition] is known to be unsatisfiable: prune path *)
              []
            else
              (* [condition] is true or unknown value: go into the branch *)
-             [Domain.ContinueProgram astate])
+             [Ok (ContinueProgram astate)])
           |> report_on_error_list analysis_data
       | Call (ret, call_exp, actuals, loc, call_flags) ->
           dispatch_call analysis_data ret call_exp actuals loc call_flags astate
@@ -393,7 +407,7 @@ module PulseTransferFunctions = struct
               ~init:[] astates
           in
           if Procname.is_java (Procdesc.get_proc_name proc_desc) then
-            remove_vars vars [Domain.ContinueProgram astate]
+            remove_vars vars [ContinueProgram astate]
           else
             (* Here we add and execute calls to dealloc for Objective-C objects
                before removing the variables *)
@@ -411,7 +425,7 @@ module PulseTransferFunctions = struct
       | Metadata (VariableLifetimeBegins (pvar, typ, location)) when not (Pvar.is_global pvar) ->
           [PulseOperations.realloc_pvar pvar typ location astate |> Domain.continue]
       | Metadata (Abstract _ | VariableLifetimeBegins _ | Nullify _ | Skip) ->
-          [Domain.ContinueProgram astate] )
+          [ContinueProgram astate] )
 
 
   let exec_instr astate analysis_data cfg_node instr =
diff --git a/infer/src/pulse/PulseExecutionDomain.ml b/infer/src/pulse/PulseExecutionDomain.ml
index 48cdb076c..7dbba75dd 100644
--- a/infer/src/pulse/PulseExecutionDomain.ml
+++ b/infer/src/pulse/PulseExecutionDomain.ml
@@ -78,33 +78,32 @@ let is_unsat_cheap exec_state = PathCondition.is_unsat_cheap (get_astate exec_st
 
 type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson_of]
 
-let summary_of_posts_common ~continue_program pdesc posts =
+let summary_of_post_common ~continue_program proc_desc = function
+  | ContinueProgram astate | ISLLatentMemoryError astate -> (
+    match AbductiveDomain.summary_of_post proc_desc astate with
+    | Unsat ->
+        None
+    | Sat astate ->
+        Some (continue_program astate) )
+  (* already a summary but need to reconstruct the variants to make the type system happy *)
+  | AbortProgram astate ->
+      Some (AbortProgram astate)
+  | ExitProgram astate ->
+      Some (ExitProgram astate)
+  | LatentAbortProgram {astate; latent_issue} ->
+      Some (LatentAbortProgram {astate; latent_issue})
+
+
+let summary_of_posts proc_desc posts =
   List.filter_mapi posts ~f:(fun i exec_state ->
       L.d_printfln "Creating spec out of state #%d:@\n%a" i pp exec_state ;
-      match exec_state with
-      | ContinueProgram astate | ISLLatentMemoryError astate -> (
-        match AbductiveDomain.summary_of_post pdesc astate with
-        | Unsat ->
-            None
-        | Sat astate ->
-            Some (continue_program astate) )
-      (* already a summary but need to reconstruct the variants to make the type system happy *)
-      | AbortProgram astate ->
-          Some (AbortProgram astate)
-      | ExitProgram astate ->
-          Some (ExitProgram astate)
-      | LatentAbortProgram {astate; latent_issue} ->
-          Some (LatentAbortProgram {astate; latent_issue}) )
-
-
-let summary_of_posts =
-  summary_of_posts_common ~continue_program:(fun astate ->
-      match (astate :> AbductiveDomain.t).isl_status with
-      | ISLOk ->
-          ContinueProgram astate
-      | ISLError ->
-          ISLLatentMemoryError astate )
-
-
-let force_exit_program =
-  summary_of_posts_common ~continue_program:(fun astate -> ExitProgram astate)
+      summary_of_post_common proc_desc exec_state ~continue_program:(fun astate ->
+          match (astate :> AbductiveDomain.t).isl_status with
+          | ISLOk ->
+              ContinueProgram astate
+          | ISLError ->
+              ISLLatentMemoryError astate ) )
+
+
+let force_exit_program proc_desc post =
+  summary_of_post_common proc_desc post ~continue_program:(fun astate -> ExitProgram astate)
diff --git a/infer/src/pulse/PulseExecutionDomain.mli b/infer/src/pulse/PulseExecutionDomain.mli
index a1080e536..972b113a5 100644
--- a/infer/src/pulse/PulseExecutionDomain.mli
+++ b/infer/src/pulse/PulseExecutionDomain.mli
@@ -36,4 +36,4 @@ type summary = AbductiveDomain.summary base_t [@@deriving compare, equal, yojson
 
 val summary_of_posts : Procdesc.t -> t list -> summary list
 
-val force_exit_program : Procdesc.t -> t list -> t list
+val force_exit_program : Procdesc.t -> t -> t option
diff --git a/infer/src/pulse/PulseModels.ml b/infer/src/pulse/PulseModels.ml
index 64da377bc..747840027 100644
--- a/infer/src/pulse/PulseModels.ml
+++ b/infer/src/pulse/PulseModels.ml
@@ -6,9 +6,9 @@
  *)
 
 open! IStd
-open IResult.Let_syntax
 open PulseBasicInterface
 open PulseDomainInterface
+open PulseOperations.Import
 
 type arg_payload = AbstractValue.t * ValueHistory.t
 
@@ -18,16 +18,16 @@ type model =
   -> Location.t
   -> ret:Ident.t * Typ.t
   -> AbductiveDomain.t
-  -> ExecutionDomain.t list PulseOperations.access_result
+  -> ExecutionDomain.t PulseOperations.access_result list
 
-let ok_continue post = Ok [ExecutionDomain.ContinueProgram post]
+let ok_continue post = [Ok (ContinueProgram post)]
 
 let cpp_model_namespace = QualifiedCppName.of_list ["__infer_pulse_model"]
 
 module Misc = struct
   let shallow_copy_value location event ret_id dest_pointer_hist src_value_hist astate =
-    let* astate, obj_copy = PulseOperations.shallow_copy location src_value_hist astate in
-    let+ astate =
+    let<*> astate, obj_copy = PulseOperations.shallow_copy location src_value_hist astate in
+    let<+> astate =
       PulseOperations.write_deref location ~ref:dest_pointer_hist
         ~obj:(fst obj_copy, event :: snd obj_copy)
         astate
@@ -36,7 +36,7 @@ module Misc = struct
 
 
   let shallow_copy location event ret_id dest_pointer_hist src_pointer_hist astate =
-    let* astate, obj =
+    let<*> astate, obj =
       PulseOperations.eval_access Read location src_pointer_hist Dereference astate
     in
     shallow_copy_value location event ret_id dest_pointer_hist obj astate
@@ -45,17 +45,16 @@ module Misc = struct
   let shallow_copy_model model_desc dest_pointer_hist src_pointer_hist : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in
-    let+ astate = shallow_copy location event ret_id dest_pointer_hist src_pointer_hist astate in
-    [ExecutionDomain.ContinueProgram astate]
+    shallow_copy location event ret_id dest_pointer_hist src_pointer_hist astate
 
 
   let early_exit : model =
    fun {proc_desc} ~callee_procname:_ _ ~ret:_ astate ->
     match AbductiveDomain.summary_of_post proc_desc astate with
     | Unsat ->
-        Ok []
+        []
     | Sat astate ->
-        Ok [ExecutionDomain.ExitProgram astate]
+        [Ok (ExitProgram astate)]
 
 
   let return_int : Int64.t -> model =
@@ -96,10 +95,8 @@ module Misc = struct
       AnalysisCallbacks.proc_resolve_attributes callee_procname
       |> Option.map ~f:ProcAttributes.get_pvar_formals
     in
-    Ok
-      [ ExecutionDomain.ContinueProgram
-          (PulseOperations.unknown_call location (Model skip_reason) ~ret ~actuals ~formals_opt
-             astate) ]
+    PulseOperations.unknown_call location (Model skip_reason) ~ret ~actuals ~formals_opt astate
+    |> ok_continue
 
 
   (** don't actually do nothing, apply the heuristics for unknown calls (this may or may not be a
@@ -129,13 +126,14 @@ module Misc = struct
         match operation with `Free -> Invalidation.CFree | `Delete -> Invalidation.CppDelete
       in
       if Config.pulse_isl then
-        let+ astates =
-          PulseOperations.invalidate_biad_isl location invalidation deleted_access astate
-        in
-        List.map astates ~f:(fun astate -> ExecutionDomain.ContinueProgram astate)
+        match PulseOperations.invalidate_biad_isl location invalidation deleted_access astate with
+        | Error _ as err ->
+            [err]
+        | Ok astates ->
+            List.map astates ~f:(fun astate -> Ok (ContinueProgram astate))
       else
-        let+ astate = PulseOperations.invalidate location invalidation deleted_access astate in
-        [ExecutionDomain.ContinueProgram astate]
+        let<+> astate = PulseOperations.invalidate location invalidation deleted_access astate in
+        astate
 end
 
 module C = struct
@@ -160,11 +158,14 @@ module C = struct
       |> PulseOperations.allocate callee_procname location ret_value
       |> set_uninitialized size_exp_opt location ret_addr
     in
-    let+ astate_null =
-      PulseArithmetic.and_eq_int ret_addr IntLit.zero astate
-      |> PulseOperations.invalidate location (ConstantDereference IntLit.zero) ret_value
+    let result_null =
+      let+ astate_null =
+        PulseArithmetic.and_eq_int ret_addr IntLit.zero astate
+        |> PulseOperations.invalidate location (ConstantDereference IntLit.zero) ret_value
+      in
+      ContinueProgram astate_null
     in
-    [ExecutionDomain.ContinueProgram astate_alloc; ExecutionDomain.ContinueProgram astate_null]
+    [Ok (ContinueProgram astate_alloc); result_null]
 
 
   let malloc_not_null_common ~size_exp_opt : model =
@@ -217,19 +218,19 @@ module ObjC = struct
 
 
   let dispatch_sync args : model =
-   fun {analyze_dependency; proc_desc; tenv; err_log} ~callee_procname:_ location ~ret astate ->
+   fun {analyze_dependency; proc_desc} ~callee_procname:_ location ~ret astate ->
     match List.last args with
     | None ->
-        Ok [ExecutionDomain.ContinueProgram astate]
+        ok_continue astate
     | Some {ProcnameDispatcher.Call.FuncArg.arg_payload= lambda_ptr_hist} -> (
-        let* astate, (lambda, _) =
+        let<*> astate, (lambda, _) =
           PulseOperations.eval_access Read location lambda_ptr_hist Dereference astate
         in
         match AddressAttributes.get_closure_proc_name lambda astate with
         | None ->
-            Ok [ExecutionDomain.ContinueProgram astate]
+            ok_continue astate
         | Some callee_proc_name ->
-            PulseOperations.call ~caller_proc_desc:proc_desc tenv err_log
+            PulseOperations.call ~caller_proc_desc:proc_desc
               ~callee_data:(analyze_dependency callee_proc_name)
               location callee_proc_name ~ret ~actuals:[] ~formals_opt:None astate )
 end
@@ -262,41 +263,40 @@ module Optional = struct
 
   let assign_none this ~desc : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
-    let* astate, value = assign_value_fresh location this ~desc astate in
+    let<*> astate, value = assign_value_fresh location this ~desc astate in
     let astate = PulseArithmetic.and_eq_int (fst value) IntLit.zero astate in
-    let+ astate = PulseOperations.invalidate location Invalidation.OptionalEmpty value astate in
-    [ExecutionDomain.ContinueProgram astate]
+    let<+> astate = PulseOperations.invalidate location Invalidation.OptionalEmpty value astate in
+    astate
 
 
   let assign_value this _value ~desc : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     (* TODO: call the copy constructor of a value *)
-    let+ astate, value = assign_value_fresh location this ~desc astate in
-    let astate = PulseArithmetic.and_positive (fst value) astate in
-    [ExecutionDomain.ContinueProgram astate]
+    let<+> astate, value = assign_value_fresh location this ~desc astate in
+    PulseArithmetic.and_positive (fst value) astate
 
 
   let assign_optional_value this init ~desc : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
-    let* astate, value = to_internal_value_deref Read location init astate in
-    let+ astate, _ = write_value location this ~value ~desc astate in
-    [ExecutionDomain.ContinueProgram astate]
+    let<*> astate, value = to_internal_value_deref Read location init astate in
+    let<+> astate, _ = write_value location this ~value ~desc astate in
+    astate
 
 
   let emplace optional ~desc : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
-    let+ astate, _ = assign_value_fresh location optional ~desc astate in
-    [ExecutionDomain.ContinueProgram astate]
+    let<+> astate, _ = assign_value_fresh location optional ~desc astate in
+    astate
 
 
   let value optional ~desc : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let* astate, ((value_addr, value_hist) as value) =
+    let<*> astate, ((value_addr, value_hist) as value) =
       to_internal_value_deref Write location optional astate
     in
     (* Check dereference to show an error at the callsite of `value()` *)
-    let* astate, _ = PulseOperations.eval_access Write location value Dereference astate in
+    let<*> astate, _ = PulseOperations.eval_access Write location value Dereference astate in
     PulseOperations.write_id ret_id (value_addr, event :: value_hist) astate |> ok_continue
 
 
@@ -304,51 +304,51 @@ module Optional = struct
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let ret_addr = AbstractValue.mk_fresh () in
     let ret_value = (ret_addr, [ValueHistory.Call {f= Model desc; location; in_call= []}]) in
-    let+ astate, (value_addr, _) = to_internal_value_deref Read location optional astate in
+    let<*> astate, (value_addr, _) = to_internal_value_deref Read location optional astate in
     let astate = PulseOperations.write_id ret_id ret_value astate in
     let astate_non_empty = PulseArithmetic.and_positive value_addr astate in
     let astate_true = PulseArithmetic.and_positive ret_addr astate_non_empty in
     let astate_empty = PulseArithmetic.and_eq_int value_addr IntLit.zero astate in
     let astate_false = PulseArithmetic.and_eq_int ret_addr IntLit.zero astate_empty in
-    [ExecutionDomain.ContinueProgram astate_false; ExecutionDomain.ContinueProgram astate_true]
+    [Ok (ContinueProgram astate_false); Ok (ContinueProgram astate_true)]
 
 
   let get_pointer optional ~desc : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let* astate, value_addr = to_internal_value_deref Read location optional astate in
+    let<*> astate, value_addr = to_internal_value_deref Read location optional astate in
     let value_update_hist = (fst value_addr, event :: snd value_addr) in
     let astate_value_addr =
       PulseOperations.write_id ret_id value_update_hist astate
       |> PulseArithmetic.and_positive (fst value_addr)
     in
     let nullptr = (AbstractValue.mk_fresh (), [event]) in
-    let+ astate_null =
+    let<*> astate_null =
       PulseOperations.write_id ret_id nullptr astate
       |> PulseArithmetic.and_eq_int (fst value_addr) IntLit.zero
       |> PulseArithmetic.and_eq_int (fst nullptr) IntLit.zero
       |> PulseOperations.invalidate location (ConstantDereference IntLit.zero) nullptr
     in
-    [ExecutionDomain.ContinueProgram astate_value_addr; ExecutionDomain.ContinueProgram astate_null]
+    [Ok (ContinueProgram astate_value_addr); Ok (ContinueProgram astate_null)]
 
 
   let value_or optional default ~desc : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let* astate, value_addr = to_internal_value_deref Read location optional astate in
+    let<*> astate, value_addr = to_internal_value_deref Read location optional astate in
     let astate_non_empty = PulseArithmetic.and_positive (fst value_addr) astate in
-    let* astate_non_empty, value =
+    let<*> astate_non_empty, value =
       PulseOperations.eval_access Read location value_addr Dereference astate_non_empty
     in
     let value_update_hist = (fst value, event :: snd value) in
     let astate_value = PulseOperations.write_id ret_id value_update_hist astate_non_empty in
-    let+ astate, (default_val, default_hist) =
+    let<*> astate, (default_val, default_hist) =
       PulseOperations.eval_access Read location default Dereference astate
     in
     let default_value_hist = (default_val, event :: default_hist) in
     let astate_empty = PulseArithmetic.and_eq_int (fst value_addr) IntLit.zero astate in
     let astate_default = PulseOperations.write_id ret_id default_value_hist astate_empty in
-    [ExecutionDomain.ContinueProgram astate_value; ExecutionDomain.ContinueProgram astate_default]
+    [Ok (ContinueProgram astate_value); Ok (ContinueProgram astate_default)]
 end
 
 module Cplusplus = struct
@@ -385,12 +385,12 @@ module StdAtomicInteger = struct
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "std::atomic::atomic()"; location; in_call= []} in
     let this = (AbstractValue.mk_fresh (), [event]) in
-    let* astate, int_field =
+    let<*> astate, int_field =
       PulseOperations.eval_access Write location this (FieldAccess internal_int) astate
     in
-    let* astate = PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate in
-    let+ astate = PulseOperations.write_deref location ~ref:this_address ~obj:this astate in
-    [ExecutionDomain.ContinueProgram astate]
+    let<*> astate = PulseOperations.write_deref location ~ref:int_field ~obj:init_value astate in
+    let<+> astate = PulseOperations.write_deref location ~ref:this_address ~obj:this astate in
+    astate
 
 
   let arith_bop prepost location event ret_id bop this operand astate =
@@ -409,30 +409,30 @@ module StdAtomicInteger = struct
   let fetch_add this (increment, _) _memory_ordering : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "std::atomic::fetch_add()"; location; in_call= []} in
-    let+ astate =
+    let<+> astate =
       arith_bop `Post location event ret_id (PlusA None) this (AbstractValueOperand increment)
         astate
     in
-    [ExecutionDomain.ContinueProgram astate]
+    astate
 
 
   let fetch_sub this (increment, _) _memory_ordering : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "std::atomic::fetch_sub()"; location; in_call= []} in
-    let+ astate =
+    let<+> astate =
       arith_bop `Post location event ret_id (MinusA None) this (AbstractValueOperand increment)
         astate
     in
-    [ExecutionDomain.ContinueProgram astate]
+    astate
 
 
   let operator_plus_plus_pre this : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "std::atomic::operator++()"; location; in_call= []} in
-    let+ astate =
+    let<+> astate =
       arith_bop `Pre location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate
     in
-    [ExecutionDomain.ContinueProgram astate]
+    astate
 
 
   let operator_plus_plus_post this _int : model =
@@ -440,19 +440,19 @@ module StdAtomicInteger = struct
     let event =
       ValueHistory.Call {f= Model "std::atomic<T>::operator++(T)"; location; in_call= []}
     in
-    let+ astate =
+    let<+> astate =
       arith_bop `Post location event ret_id (PlusA None) this (LiteralOperand IntLit.one) astate
     in
-    [ExecutionDomain.ContinueProgram astate]
+    astate
 
 
   let operator_minus_minus_pre this : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "std::atomic::operator--()"; location; in_call= []} in
-    let+ astate =
+    let<+> astate =
       arith_bop `Pre location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate
     in
-    [ExecutionDomain.ContinueProgram astate]
+    astate
 
 
   let operator_minus_minus_post this _int : model =
@@ -460,18 +460,17 @@ module StdAtomicInteger = struct
     let event =
       ValueHistory.Call {f= Model "std::atomic<T>::operator--(T)"; location; in_call= []}
     in
-    let+ astate =
+    let<+> astate =
       arith_bop `Post location event ret_id (MinusA None) this (LiteralOperand IntLit.one) astate
     in
-    [ExecutionDomain.ContinueProgram astate]
+    astate
 
 
   let load_instr model_desc this _memory_ordering_opt : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model model_desc; location; in_call= []} in
-    let+ astate, _int_addr, (int, hist) = load_backing_int location this astate in
-    let astate = PulseOperations.write_id ret_id (int, event :: hist) astate in
-    [ExecutionDomain.ContinueProgram astate]
+    let<+> astate, _int_addr, (int, hist) = load_backing_int location this astate in
+    PulseOperations.write_id ret_id (int, event :: hist) astate
 
 
   let load = load_instr "std::atomic<T>::load()"
@@ -489,17 +488,16 @@ module StdAtomicInteger = struct
   let store this_address (new_value, new_hist) _memory_ordering : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "std::atomic::store()"; location; in_call= []} in
-    let+ astate = store_backing_int location this_address (new_value, event :: new_hist) astate in
-    [ExecutionDomain.ContinueProgram astate]
+    let<+> astate = store_backing_int location this_address (new_value, event :: new_hist) astate in
+    astate
 
 
   let exchange this_address (new_value, new_hist) _memory_ordering : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "std::atomic::exchange()"; location; in_call= []} in
-    let* astate, _int_addr, (old_int, old_hist) = load_backing_int location this_address astate in
-    let+ astate = store_backing_int location this_address (new_value, event :: new_hist) astate in
-    let astate = PulseOperations.write_id ret_id (old_int, event :: old_hist) astate in
-    [ExecutionDomain.ContinueProgram astate]
+    let<*> astate, _int_addr, (old_int, old_hist) = load_backing_int location this_address astate in
+    let<+> astate = store_backing_int location this_address (new_value, event :: new_hist) astate in
+    PulseOperations.write_id ret_id (old_int, event :: old_hist) astate
 end
 
 module JavaObject = struct
@@ -507,12 +505,11 @@ module JavaObject = struct
   let clone src_pointer_hist : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "Object.clone"; location; in_call= []} in
-    let* astate, obj =
+    let<*> astate, obj =
       PulseOperations.eval_access Read location src_pointer_hist Dereference astate
     in
-    let+ astate, obj_copy = PulseOperations.shallow_copy location obj astate in
-    let astate = PulseOperations.write_id ret_id (fst obj_copy, event :: snd obj_copy) astate in
-    [ExecutionDomain.ContinueProgram astate]
+    let<+> astate, obj_copy = PulseOperations.shallow_copy location obj astate in
+    PulseOperations.write_id ret_id (fst obj_copy, event :: snd obj_copy) astate
 end
 
 module StdBasicString = struct
@@ -531,52 +528,49 @@ module StdBasicString = struct
   let data this_hist : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "std::basic_string::data()"; location; in_call= []} in
-    let* astate, string_addr_hist = to_internal_string location this_hist astate in
-    let+ astate, (string, hist) =
+    let<*> astate, string_addr_hist = to_internal_string location this_hist astate in
+    let<+> astate, (string, hist) =
       PulseOperations.eval_access Read location string_addr_hist Dereference astate
     in
-    let astate = PulseOperations.write_id ret_id (string, event :: hist) astate in
-    [ExecutionDomain.ContinueProgram astate]
+    PulseOperations.write_id ret_id (string, event :: hist) astate
 
 
   let destructor this_hist : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let model = CallEvent.Model "std::basic_string::~basic_string()" in
     let call_event = ValueHistory.Call {f= model; location; in_call= []} in
-    let* astate, (string_addr, string_hist) = to_internal_string location this_hist astate in
+    let<*> astate, (string_addr, string_hist) = to_internal_string location this_hist astate in
     let string_addr_hist = (string_addr, call_event :: string_hist) in
-    let* astate =
+    let<*> astate =
       PulseOperations.invalidate_access location CppDelete string_addr_hist Dereference astate
     in
-    let+ astate = PulseOperations.invalidate location CppDelete string_addr_hist astate in
-    [ExecutionDomain.ContinueProgram astate]
+    let<+> astate = PulseOperations.invalidate location CppDelete string_addr_hist astate in
+    astate
 end
 
 module StdFunction = struct
   let operator_call ProcnameDispatcher.Call.FuncArg.{arg_payload= lambda_ptr_hist; typ} actuals :
       model =
-   fun {analyze_dependency; proc_desc; tenv; err_log} ~callee_procname:_ location ~ret astate ->
+   fun {analyze_dependency; proc_desc} ~callee_procname:_ location ~ret astate ->
     let havoc_ret (ret_id, _) astate =
       let event = ValueHistory.Call {f= Model "std::function::operator()"; location; in_call= []} in
       [PulseOperations.havoc_id ret_id [event] astate]
     in
-    let* astate, (lambda, _) =
+    let<*> astate, (lambda, _) =
       PulseOperations.eval_access Read location lambda_ptr_hist Dereference astate
     in
-    let* astate = PulseOperations.Closures.check_captured_addresses location lambda astate in
+    let<*> astate = PulseOperations.Closures.check_captured_addresses location lambda astate in
     match AddressAttributes.get_closure_proc_name lambda astate with
     | None ->
         (* we don't know what proc name this lambda resolves to *)
-        Ok
-          ( havoc_ret ret astate
-          |> List.map ~f:(fun astate -> ExecutionDomain.ContinueProgram astate) )
+        havoc_ret ret astate |> List.map ~f:(fun astate -> Ok (ContinueProgram astate))
     | Some callee_proc_name ->
         let actuals =
           (lambda_ptr_hist, typ)
           :: List.map actuals ~f:(fun ProcnameDispatcher.Call.FuncArg.{arg_payload; typ} ->
                  (arg_payload, typ) )
         in
-        PulseOperations.call ~caller_proc_desc:proc_desc tenv err_log
+        PulseOperations.call ~caller_proc_desc:proc_desc
           ~callee_data:(analyze_dependency callee_proc_name)
           location callee_proc_name ~ret ~actuals ~formals_opt:None astate
 
@@ -584,21 +578,18 @@ module StdFunction = struct
   let assign dest ProcnameDispatcher.Call.FuncArg.{arg_payload= src; typ= src_typ} ~desc : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let+ astate =
-      if PulseArithmetic.is_known_zero astate (fst src) then
-        let empty_target = AbstractValue.mk_fresh () in
-        let+ astate =
-          PulseOperations.write_deref location ~ref:dest ~obj:(empty_target, [event]) astate
-        in
-        PulseOperations.havoc_id ret_id [event] astate
-      else
-        match src_typ.Typ.desc with
-        | Tptr (_, Pk_reference) ->
-            Misc.shallow_copy location event ret_id dest src astate
-        | _ ->
-            Misc.shallow_copy_value location event ret_id dest src astate
-    in
-    [ExecutionDomain.ContinueProgram astate]
+    if PulseArithmetic.is_known_zero astate (fst src) then
+      let empty_target = AbstractValue.mk_fresh () in
+      let<+> astate =
+        PulseOperations.write_deref location ~ref:dest ~obj:(empty_target, [event]) astate
+      in
+      PulseOperations.havoc_id ret_id [event] astate
+    else
+      match src_typ.Typ.desc with
+      | Tptr (_, Pk_reference) ->
+          Misc.shallow_copy location event ret_id dest src astate
+      | _ ->
+          Misc.shallow_copy_value location event ret_id dest src astate
 end
 
 module GenericArrayBackedCollection = struct
@@ -689,14 +680,15 @@ module GenericArrayBackedCollectionIterator = struct
   let constructor ~desc this init : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    construct location event ~init ~ref:this astate >>| ExecutionDomain.continue >>| List.return
+    let<+> astate = construct location event ~init ~ref:this astate in
+    astate
 
 
-  let operator_compare comparison ~desc iter_lhs iter_rhs _ ~callee_procname:_ location
-      ~ret:(ret_id, _) astate =
+  let operator_compare comparison ~desc iter_lhs iter_rhs : model =
+   fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let* astate, _, (index_lhs, _) = to_internal_pointer_deref Read location iter_lhs astate in
-    let+ astate, _, (index_rhs, _) = to_internal_pointer_deref Read location iter_rhs astate in
+    let<*> astate, _, (index_lhs, _) = to_internal_pointer_deref Read location iter_lhs astate in
+    let<*> astate, _, (index_rhs, _) = to_internal_pointer_deref Read location iter_rhs astate in
     let ret_val = AbstractValue.mk_fresh () in
     let astate = PulseOperations.write_id ret_id (ret_val, [event]) astate in
     let ret_val_equal, ret_val_notequal =
@@ -716,24 +708,29 @@ module GenericArrayBackedCollectionIterator = struct
       |> PulseArithmetic.prune_binop ~negated:false Ne (AbstractValueOperand index_lhs)
            (AbstractValueOperand index_rhs)
     in
-    [ExecutionDomain.ContinueProgram astate_equal; ExecutionDomain.ContinueProgram astate_notequal]
+    [Ok (ContinueProgram astate_equal); Ok (ContinueProgram astate_notequal)]
 
 
-  let operator_star ~desc iter _ ~callee_procname:_ location ~ret astate =
+  let operator_star ~desc iter : model =
+   fun _ ~callee_procname:_ location ~ret astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let+ astate, pointer, (elem, _) = to_elem_pointed_by_iterator Read location iter astate in
-    let astate = PulseOperations.write_id (fst ret) (elem, event :: snd pointer) astate in
-    [ExecutionDomain.ContinueProgram astate]
+    let<+> astate, pointer, (elem, _) = to_elem_pointed_by_iterator Read location iter astate in
+    PulseOperations.write_id (fst ret) (elem, event :: snd pointer) astate
 
 
-  let operator_step step ~desc iter _ ~callee_procname:_ location ~ret:_ astate =
+  let operator_step step ~desc iter : model =
+   fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
     let index_new = AbstractValue.mk_fresh () in
-    let* astate, pointer, _ =
+    let<*> astate, pointer, _ =
       to_elem_pointed_by_iterator Read ~step:(Some step) location iter astate
     in
-    PulseOperations.write_deref location ~ref:pointer ~obj:(index_new, event :: snd pointer) astate
-    >>| ExecutionDomain.continue >>| List.return
+    let<+> astate =
+      PulseOperations.write_deref location ~ref:pointer
+        ~obj:(index_new, event :: snd pointer)
+        astate
+    in
+    astate
 end
 
 module JavaIterator = struct
@@ -741,54 +738,54 @@ module JavaIterator = struct
    fun _ ~callee_procname:_ location ~ret astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
     let ref = (AbstractValue.mk_fresh (), [event]) in
-    let+ astate = GenericArrayBackedCollectionIterator.construct location event ~init ~ref astate in
-    let astate = PulseOperations.write_id (fst ret) ref astate in
-    [ExecutionDomain.ContinueProgram astate]
+    let<+> astate =
+      GenericArrayBackedCollectionIterator.construct location event ~init ~ref astate
+    in
+    PulseOperations.write_id (fst ret) ref astate
 
 
   (* {curr -> v_c} is modified to {curr -> v_fresh} and returns array[v_c] *)
-  let next ~desc iter _ ~callee_procname:_ location ~ret astate =
+  let next ~desc iter : model =
+   fun _ ~callee_procname:_ location ~ret astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
     let new_index = AbstractValue.mk_fresh () in
-    let* astate, (curr_index, curr_index_hist) =
+    let<*> astate, (curr_index, curr_index_hist) =
       GenericArrayBackedCollectionIterator.to_internal_pointer Read location iter astate
     in
-    let* astate, (curr_elem_val, curr_elem_hist) =
+    let<*> astate, (curr_elem_val, curr_elem_hist) =
       GenericArrayBackedCollection.element location iter curr_index astate
     in
-    let+ astate =
+    let<+> astate =
       PulseOperations.write_field location ~ref:iter
         GenericArrayBackedCollectionIterator.internal_pointer
         ~obj:(new_index, event :: curr_index_hist)
         astate
     in
-    let astate =
-      PulseOperations.write_id (fst ret) (curr_elem_val, event :: curr_elem_hist) astate
-    in
-    [ExecutionDomain.ContinueProgram astate]
+    PulseOperations.write_id (fst ret) (curr_elem_val, event :: curr_elem_hist) astate
 
 
   (* {curr -> v_c } is modified to {curr -> v_fresh} and writes to array[v_c] *)
-  let remove ~desc iter _ ~callee_procname:_ location ~ret:_ astate =
+  let remove ~desc iter : model =
+   fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
     let new_index = AbstractValue.mk_fresh () in
-    let* astate, (curr_index, curr_index_hist) =
+    let<*> astate, (curr_index, curr_index_hist) =
       GenericArrayBackedCollectionIterator.to_internal_pointer Read location iter astate
     in
-    let* astate =
+    let<*> astate =
       PulseOperations.write_field location ~ref:iter
         GenericArrayBackedCollectionIterator.internal_pointer
         ~obj:(new_index, event :: curr_index_hist)
         astate
     in
     let new_elem = AbstractValue.mk_fresh () in
-    let* astate, arr = GenericArrayBackedCollection.eval Read location iter astate in
-    let+ astate =
+    let<*> astate, arr = GenericArrayBackedCollection.eval Read location iter astate in
+    let<+> astate =
       PulseOperations.write_arr_index location ~ref:arr ~index:curr_index
         ~obj:(new_elem, event :: curr_index_hist)
         astate
     in
-    [ExecutionDomain.ContinueProgram astate]
+    astate
 end
 
 module StdVector = struct
@@ -802,15 +799,16 @@ module StdVector = struct
     >>= PulseOperations.havoc_field location vector GenericArrayBackedCollection.field trace
 
 
-  let init_list_constructor this init_list _ ~callee_procname:_ location ~ret:_ astate =
+  let init_list_constructor this init_list : model =
+   fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "std::vector::vector()"; location; in_call= []} in
-    let* astate, init_copy = PulseOperations.shallow_copy location init_list astate in
-    let+ astate =
+    let<*> astate, init_copy = PulseOperations.shallow_copy location init_list astate in
+    let<+> astate =
       PulseOperations.write_field location ~ref:this GenericArrayBackedCollection.field
         ~obj:(fst init_copy, event :: snd init_copy)
         astate
     in
-    [ExecutionDomain.ContinueProgram astate]
+    astate
 
 
   let invalidate_references vector_f vector : model =
@@ -821,18 +819,17 @@ module StdVector = struct
         ; location
         ; in_call= [] }
     in
-    reallocate_internal_array [crumb] vector vector_f location astate
-    >>| ExecutionDomain.continue >>| List.return
+    let<+> astate = reallocate_internal_array [crumb] vector vector_f location astate in
+    astate
 
 
   let at ~desc vector index : model =
    fun _ ~callee_procname:_ location ~ret astate ->
     let event = ValueHistory.Call {f= Model desc; location; in_call= []} in
-    let+ astate, (addr, hist) =
+    let<+> astate, (addr, hist) =
       GenericArrayBackedCollection.element location vector (fst index) astate
     in
-    let astate = PulseOperations.write_id (fst ret) (addr, event :: hist) astate in
-    [ExecutionDomain.ContinueProgram astate]
+    PulseOperations.write_id (fst ret) (addr, event :: hist) astate
 
 
   let vector_begin vector iter : model =
@@ -842,44 +839,48 @@ module StdVector = struct
     let pointer_val = (AbstractValue.mk_fresh (), pointer_hist) in
     let index_zero = AbstractValue.mk_fresh () in
     let astate = PulseArithmetic.and_eq_int index_zero IntLit.zero astate in
-    let* astate, ((arr_addr, _) as arr) =
+    let<*> astate, ((arr_addr, _) as arr) =
       GenericArrayBackedCollection.eval Read location vector astate
     in
-    let* astate, _ = GenericArrayBackedCollection.eval_element location arr index_zero astate in
-    PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field
-      ~obj:(arr_addr, pointer_hist) astate
-    >>= PulseOperations.write_field location ~ref:iter
-          GenericArrayBackedCollectionIterator.internal_pointer ~obj:pointer_val
-    >>= PulseOperations.write_deref location ~ref:pointer_val ~obj:(index_zero, pointer_hist)
-    >>| ExecutionDomain.continue >>| List.return
+    let<*> astate, _ = GenericArrayBackedCollection.eval_element location arr index_zero astate in
+    let<+> astate =
+      PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field
+        ~obj:(arr_addr, pointer_hist) astate
+      >>= PulseOperations.write_field location ~ref:iter
+            GenericArrayBackedCollectionIterator.internal_pointer ~obj:pointer_val
+      >>= PulseOperations.write_deref location ~ref:pointer_val ~obj:(index_zero, pointer_hist)
+    in
+    astate
 
 
   let vector_end vector iter : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "std::vector::end()"; location; in_call= []} in
-    let* astate, (arr_addr, _) = GenericArrayBackedCollection.eval Read location vector astate in
-    let* astate, (pointer_addr, _) =
+    let<*> astate, (arr_addr, _) = GenericArrayBackedCollection.eval Read location vector astate in
+    let<*> astate, (pointer_addr, _) =
       GenericArrayBackedCollection.eval_pointer_to_last_element location vector astate
     in
     let pointer_hist = event :: snd iter in
     let pointer_val = (pointer_addr, pointer_hist) in
-    let* astate =
+    let<*> astate =
       PulseOperations.write_field location ~ref:iter GenericArrayBackedCollection.field
         ~obj:(arr_addr, pointer_hist) astate
     in
-    let+ astate =
+    let<+> astate =
       PulseOperations.write_field location ~ref:iter
         GenericArrayBackedCollectionIterator.internal_pointer ~obj:pointer_val astate
     in
-    [ExecutionDomain.ContinueProgram astate]
+    astate
 
 
   let reserve vector : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let crumb = ValueHistory.Call {f= Model "std::vector::reserve()"; location; in_call= []} in
-    reallocate_internal_array [crumb] vector Reserve location astate
-    >>| AddressAttributes.std_vector_reserve (fst vector)
-    >>| ExecutionDomain.continue >>| List.return
+    let<+> astate =
+      reallocate_internal_array [crumb] vector Reserve location astate
+      >>| AddressAttributes.std_vector_reserve (fst vector)
+    in
+    astate
 
 
   let push_back vector : model =
@@ -891,18 +892,17 @@ module StdVector = struct
       ok_continue astate
     else
       (* simulate a re-allocation of the underlying array every time an element is added *)
-      reallocate_internal_array [crumb] vector PushBack location astate
-      >>| ExecutionDomain.continue >>| List.return
+      let<+> astate = reallocate_internal_array [crumb] vector PushBack location astate in
+      astate
 
 
   let empty vector : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let crumb = ValueHistory.Call {f= Model "std::vector::empty()"; location; in_call= []} in
-    let+ astate, (value_addr, value_hist) =
+    let<+> astate, (value_addr, value_hist) =
       GenericArrayBackedCollection.eval_is_empty location vector astate
     in
-    let astate = PulseOperations.write_id ret_id (value_addr, crumb :: value_hist) astate in
-    [ExecutionDomain.ContinueProgram astate]
+    PulseOperations.write_id ret_id (value_addr, crumb :: value_hist) astate
 end
 
 module JavaCollection = struct
@@ -910,30 +910,29 @@ module JavaCollection = struct
   let set coll (index, _) (new_elem, new_elem_hist) : model =
    fun _ ~callee_procname:_ location ~ret astate ->
     let event = ValueHistory.Call {f= Model "Collection.set"; location; in_call= []} in
-    let* astate, arr = GenericArrayBackedCollection.eval Read location coll astate in
-    let* astate, (old_addr, old_hist) =
+    let<*> astate, arr = GenericArrayBackedCollection.eval Read location coll astate in
+    let<*> astate, (old_addr, old_hist) =
       GenericArrayBackedCollection.element location coll index astate
     in
-    let+ astate =
+    let<+> astate =
       PulseOperations.write_arr_index location ~ref:arr ~index
         ~obj:(new_elem, event :: new_elem_hist)
         astate
     in
-    let astate = PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate in
-    [ExecutionDomain.ContinueProgram astate]
+    PulseOperations.write_id (fst ret) (old_addr, event :: old_hist) astate
 
 
   (* writes to arr[index]-> new_elem   *)
   let add_at coll (index, _) (new_elem, new_elem_hist) : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "Collection.add"; location; in_call= []} in
-    let* astate, arr = GenericArrayBackedCollection.eval Read location coll astate in
-    let+ astate =
+    let<*> astate, arr = GenericArrayBackedCollection.eval Read location coll astate in
+    let<+> astate =
       PulseOperations.write_arr_index location ~ref:arr ~index
         ~obj:(new_elem, event :: new_elem_hist)
         astate
     in
-    [ExecutionDomain.ContinueProgram astate]
+    astate
 
 
   (* writes to arr[index]-> new_elem where index is a fresh address *)
@@ -946,14 +945,14 @@ module JavaCollection = struct
   let remove_at coll (index, _) : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "Collection.add"; location; in_call= []} in
-    let* astate, arr = GenericArrayBackedCollection.eval Read location coll astate in
+    let<*> astate, arr = GenericArrayBackedCollection.eval Read location coll astate in
     let fresh_elem = AbstractValue.mk_fresh () in
-    let+ astate =
+    let<+> astate =
       PulseOperations.write_arr_index location ~ref:arr ~index
         ~obj:(fresh_elem, event :: snd arr)
         astate
     in
-    [ExecutionDomain.ContinueProgram astate]
+    astate
 
 
   (* writes to arr[index]-> fresh_elem where index is fresh *)
@@ -990,14 +989,14 @@ module JavaInteger = struct
   let constructor this_address init_value : model =
    fun _ ~callee_procname:_ location ~ret:_ astate ->
     let event = ValueHistory.Call {f= Model "Integer.init"; location; in_call= []} in
-    let+ state = construct this_address init_value event location astate in
-    [ExecutionDomain.continue state]
+    let<+> astate = construct this_address init_value event location astate in
+    astate
 
 
   let equals this arg : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
-    let* astate, _int_addr1, (int1, hist) = load_backing_int location this astate in
-    let* astate, _int_addr2, (int2, _) = load_backing_int location arg astate in
+    let<*> astate, _int_addr1, (int1, hist) = load_backing_int location this astate in
+    let<*> astate, _int_addr2, (int2, _) = load_backing_int location arg astate in
     let binop_addr = AbstractValue.mk_fresh () in
     let astate =
       PulseArithmetic.eval_binop binop_addr Binop.Eq (AbstractValueOperand int1)
@@ -1008,7 +1007,7 @@ module JavaInteger = struct
 
   let int_val this : model =
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
-    let* astate, _int_addr1, int_value_hist = load_backing_int location this astate in
+    let<*> astate, _int_addr1, int_value_hist = load_backing_int location this astate in
     PulseOperations.write_id ret_id int_value_hist astate |> ok_continue
 
 
@@ -1016,9 +1015,8 @@ module JavaInteger = struct
    fun _ ~callee_procname:_ location ~ret:(ret_id, _) astate ->
     let event = ValueHistory.Call {f= Model "Integer.valueOf"; location; in_call= []} in
     let new_alloc = (AbstractValue.mk_fresh (), [event]) in
-    let+ astate = construct new_alloc init_value event location astate in
-    let astate = PulseOperations.write_id ret_id new_alloc astate in
-    [ExecutionDomain.continue astate]
+    let<+> astate = construct new_alloc init_value event location astate in
+    PulseOperations.write_id ret_id new_alloc astate
 end
 
 module JavaPreconditions = struct
diff --git a/infer/src/pulse/PulseModels.mli b/infer/src/pulse/PulseModels.mli
index 6ed8aebb3..3c2cc11dd 100644
--- a/infer/src/pulse/PulseModels.mli
+++ b/infer/src/pulse/PulseModels.mli
@@ -14,7 +14,7 @@ type model =
   -> Location.t
   -> ret:Ident.t * Typ.t
   -> AbductiveDomain.t
-  -> ExecutionDomain.t list PulseOperations.access_result
+  -> ExecutionDomain.t PulseOperations.access_result list
 
 val dispatch :
      Tenv.t
diff --git a/infer/src/pulse/PulseOperations.ml b/infer/src/pulse/PulseOperations.ml
index f6805e59c..ea5c07dab 100644
--- a/infer/src/pulse/PulseOperations.ml
+++ b/infer/src/pulse/PulseOperations.ml
@@ -4,17 +4,35 @@
  * This source code is licensed under the MIT license found in the
  * LICENSE file in the root directory of this source tree.
  *)
+
 open! IStd
 module L = Logging
-open IResult.Let_syntax
 open PulseBasicInterface
 open PulseDomainInterface
 
 type t = AbductiveDomain.t
 
-type 'a access_result = 'a PulseReport.access_result
+module Import = struct
+  type access_mode = Read | Write | NoAccess
+
+  type 'abductive_domain_t base_t = 'abductive_domain_t ExecutionDomain.base_t =
+    | ContinueProgram of 'abductive_domain_t
+    | ExitProgram of AbductiveDomain.summary
+    | AbortProgram of AbductiveDomain.summary
+    | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
+    | ISLLatentMemoryError of 'abductive_domain_t
+
+  type 'a access_result = 'a PulseReport.access_result
 
-type access_mode = Read | Write | NoAccess
+  include IResult.Let_syntax
+
+  let ( let<*> ) x f = match x with Error _ as err -> [err] | Ok y -> f y
+
+  let ( let<+> ) x f =
+    match x with Error _ as err -> [err] | Ok y -> [Ok (ExecutionDomain.ContinueProgram (f y))]
+end
+
+include Import
 
 let check_addr_access access_mode location (address, history) astate =
   let access_trace = Trace.Immediate {location; history} in
@@ -665,8 +683,8 @@ let conservatively_initialize_args arg_values ({AbductiveDomain.post} as astate)
   AbstractValue.Set.fold AbductiveDomain.initialize reachable_values astate
 
 
-let call ~caller_proc_desc tenv err_log ~(callee_data : (Procdesc.t * PulseSummary.t) option)
-    call_loc callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) =
+let call ~caller_proc_desc ~(callee_data : (Procdesc.t * PulseSummary.t) option) call_loc
+    callee_pname ~ret ~actuals ~formals_opt (astate : AbductiveDomain.t) =
   let get_arg_values () = List.map actuals ~f:(fun ((value, _), _) -> value) in
   match callee_data with
   | Some (callee_proc_desc, exec_states) ->
@@ -688,7 +706,7 @@ let call ~caller_proc_desc tenv err_log ~(callee_data : (Procdesc.t * PulseSumma
                let pvar = Pvar.mk name callee_pname in
                (Var.of_pvar pvar, capture_mode) )
       in
-      let+ astate, captured_vars_with_actuals =
+      let<*> astate, captured_vars_with_actuals =
         match actuals with
         | (actual_closure, _) :: _
           when not (Procname.is_objc_block callee_pname || List.is_empty captured_vars) ->
@@ -718,15 +736,13 @@ let call ~caller_proc_desc tenv err_log ~(callee_data : (Procdesc.t * PulseSumma
             | Unsat ->
                 (* couldn't apply pre/post pair *)
                 posts
-            | Sat post -> (
-              match PulseReport.report_error caller_proc_desc tenv err_log post with
-              | Error Unsat ->
-                  posts
-              | Error (Sat post) | Ok post ->
-                  post :: posts ) )
+            | Sat post ->
+                post :: posts )
   | None ->
       (* no spec found for some reason (unknown function, ...) *)
       L.d_printfln "No spec found for %a@\n" Procname.pp callee_pname ;
-      let astate = conservatively_initialize_args (get_arg_values ()) astate in
-      unknown_call call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt astate
-      |> fun astate -> Ok [ExecutionDomain.ContinueProgram astate]
+      let astate =
+        conservatively_initialize_args (get_arg_values ()) astate
+        |> unknown_call call_loc (SkippedKnownCall callee_pname) ~ret ~actuals ~formals_opt
+      in
+      [Ok (ContinueProgram astate)]
diff --git a/infer/src/pulse/PulseOperations.mli b/infer/src/pulse/PulseOperations.mli
index 605dcbf14..fa3e7216f 100644
--- a/infer/src/pulse/PulseOperations.mli
+++ b/infer/src/pulse/PulseOperations.mli
@@ -9,17 +9,44 @@ open! IStd
 open PulseBasicInterface
 open PulseDomainInterface
 
-type t = AbductiveDomain.t
+(** For [open]ing in other modules. *)
+module Import : sig
+  type access_mode =
+    | Read
+    | Write
+    | NoAccess
+        (** The initialized-ness of the address is not checked when it evaluates a heap address
+            without actual memory access, for example, when evaluating [&x.f] we need to check
+            initialized-ness of [x], not that of [x.f]. *)
+
+  (** {2 Imported types for ease of use and so we can write variants without the corresponding
+      module prefix} *)
+
+  type 'abductive_domain_t base_t = 'abductive_domain_t ExecutionDomain.base_t =
+    | ContinueProgram of 'abductive_domain_t
+    | ExitProgram of AbductiveDomain.summary
+    | AbortProgram of AbductiveDomain.summary
+    | LatentAbortProgram of {astate: AbductiveDomain.summary; latent_issue: LatentIssue.t}
+    | ISLLatentMemoryError of 'abductive_domain_t
+
+  type 'a access_result = 'a PulseReport.access_result
+
+  (** {2 Monadic syntax} *)
+
+  include module type of IResult.Let_syntax
+
+  val ( let<*> ) : 'a access_result -> ('a -> 'b access_result list) -> 'b access_result list
+  (** monadic "bind" but not really that turns an [access_result] into a list of [access_result]s
+      (not really because the first type is not an [access_result list] but just an [access_result]) *)
+
+  val ( let<+> ) :
+    'a access_result -> ('a -> 'abductive_domain_t) -> 'abductive_domain_t base_t access_result list
+  (** monadic "map" but even less really that turns an [access_result] into an analysis result *)
+end
 
-type 'a access_result = 'a PulseReport.access_result
+include module type of Import
 
-type access_mode =
-  | Read
-  | Write
-  | NoAccess
-      (** The initialized-ness of the address is not checked when it evaluates a heap address
-          without actual memory access, for example, when evaluating [&x.f] we need to check
-          initialized-ness of [x], not that of [x.f]. *)
+type t = AbductiveDomain.t
 
 val check_addr_access :
   access_mode -> Location.t -> AbstractValue.t * ValueHistory.t -> t -> t access_result
@@ -159,8 +186,6 @@ val check_address_escape :
 
 val call :
      caller_proc_desc:Procdesc.t
-  -> Tenv.t
-  -> Errlog.t
   -> callee_data:(Procdesc.t * PulseSummary.t) option
   -> Location.t
   -> Procname.t
@@ -168,7 +193,7 @@ val call :
   -> actuals:((AbstractValue.t * ValueHistory.t) * Typ.t) list
   -> formals_opt:(Pvar.t * Typ.t) list option
   -> t
-  -> ExecutionDomain.t list access_result
+  -> ExecutionDomain.t access_result list
 (** perform an interprocedural call: apply the summary for the call proc name passed as argument if
     it exists *)