diff --git a/infer/src/backend/buckets.ml b/infer/src/backend/buckets.ml
index 0ba1ff035..a2dca318f 100644
--- a/infer/src/backend/buckets.ml
+++ b/infer/src/backend/buckets.ml
@@ -35,11 +35,12 @@ let check_nested_loop path pos_opt =
     incr trace_length;
     (* L.d_strln ("level " ^ string_of_int level ^ " (Cfg.Node.get_id node) " ^ string_of_int nid); *)
     () in
-  let f level p session exn_opt =
-    let node = Paths.Path.curr_node p in
-    do_any_node level node;
-    if level = 0 then do_node_caller node;
-    () in
+  let f level p session exn_opt = match Paths.Path.curr_node p  with
+    | Some node ->
+        do_any_node level node;
+        if level = 0 then do_node_caller node
+    | None ->
+        () in
   Paths.Path.iter_longest_sequence f pos_opt path;
   in_nested_loop ()
 
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index 8d678e6c8..e3827ffc7 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -138,22 +138,26 @@ let path_set_checkout_todo (node: Cfg.node) : Paths.PathSet.t =
 (* =============== START: Print a complete path in a dotty file =============== *)
 
 let pp_path_dotty f path =
-  let get_node_id_from_path p =
-    let node = Paths.Path.curr_node p in
-    Cfg.Node.get_id node in
   let count = ref 0 in
   let prev_n_id = ref 0 in
   let curr_n_id = ref 0 in
   prev_n_id:=- 1;
-  let g level p session exn_opt =
-    let curr_node = Paths.Path.curr_node p in
-    let curr_path_set = htable_retrieve path_set_visited (Cfg.Node.get_id curr_node) in
-    let plist = Paths.PathSet.filter_path p curr_path_set in
-    incr count;
-    curr_n_id:= (get_node_id_from_path p);
-    Dotty.pp_dotty_prop_list_in_path f plist !prev_n_id !curr_n_id;
-    L.out "@.Path #%d: %a@." !count Paths.Path.pp p;
-    prev_n_id:=!curr_n_id in
+  let get_node_id_from_path p = match Paths.Path.curr_node p with
+    | Some node ->
+        Cfg.Node.get_id node
+    | None ->
+        !curr_n_id in
+  let g level p session exn_opt = match Paths.Path.curr_node p with
+    | Some curr_node ->
+        let curr_path_set = htable_retrieve path_set_visited (Cfg.Node.get_id curr_node) in
+        let plist = Paths.PathSet.filter_path p curr_path_set in
+        incr count;
+        curr_n_id := get_node_id_from_path p;
+        Dotty.pp_dotty_prop_list_in_path f plist !prev_n_id !curr_n_id;
+        L.out "@.Path #%d: %a@." !count Paths.Path.pp p;
+        prev_n_id:=!curr_n_id
+    | None ->
+        () in
   L.out "@.@.Printing Path: %a to file error_path.dot@." Paths.Path.pp path;
   Dotty.reset_proposition_counter ();
   Dotty.reset_dotty_spec_counter ();
@@ -335,18 +339,20 @@ let reset_prop_metrics () =
 let d_path (path, pos_opt) =
   let step = ref 0 in
   let prop_last_step = ref Prop.prop_emp in (* if the last step had a singleton prop, store it here *)
-  let f level p session exn_opt =
-    let curr_node = Paths.Path.curr_node p in
-    let curr_path_set = htable_retrieve path_set_visited (Cfg.Node.get_id curr_node) in
-    let plist = Paths.PathSet.filter_path p curr_path_set in
-    incr step;
-    (* Propset.pp_proplist_dotty_file ("path" ^ (string_of_int !count) ^ ".dot") plist; *)
-    L.d_strln ("Path Step #" ^ string_of_int !step ^
-               " node " ^ string_of_int (Cfg.Node.get_id curr_node) ^
-               " session " ^ string_of_int session ^ ":");
-    Propset.d !prop_last_step (Propset.from_proplist plist); L.d_ln ();
-    Cfg.Node.d_instrs true None curr_node; L.d_ln (); L.d_ln ();
-    prop_last_step := (match plist with | [prop] -> prop | _ -> Prop.prop_emp) in
+  let f level p session exn_opt = match Paths.Path.curr_node p with
+    | Some curr_node ->
+        let curr_path_set = htable_retrieve path_set_visited (Cfg.Node.get_id curr_node) in
+        let plist = Paths.PathSet.filter_path p curr_path_set in
+        incr step;
+        (* Propset.pp_proplist_dotty_file ("path" ^ (string_of_int !count) ^ ".dot") plist; *)
+        L.d_strln ("Path Step #" ^ string_of_int !step ^
+                   " node " ^ string_of_int (Cfg.Node.get_id curr_node) ^
+                   " session " ^ string_of_int session ^ ":");
+        Propset.d !prop_last_step (Propset.from_proplist plist); L.d_ln ();
+        Cfg.Node.d_instrs true None curr_node; L.d_ln (); L.d_ln ();
+        prop_last_step := (match plist with | [prop] -> prop | _ -> Prop.prop_emp)
+    | None ->
+        () in
   L.d_str "Path: "; Paths.Path.d_stats path; L.d_ln ();
   Paths.Path.d path; L.d_ln ();
   (* pp_complete_path_dotty_file path; *)
diff --git a/infer/src/backend/paths.ml b/infer/src/backend/paths.ml
index 872a0b49d..2f37ff023 100644
--- a/infer/src/backend/paths.ml
+++ b/infer/src/backend/paths.ml
@@ -35,7 +35,7 @@ module Path : sig
   val create_loc_trace : t -> Sil.path_pos option -> Errlog.loc_trace
 
   (** return the current node of the path *)
-  val curr_node : t -> Cfg.node
+  val curr_node : t -> Cfg.node option
 
   (** dump a path *)
   val d : t -> unit
@@ -115,10 +115,11 @@ end = struct
     stats.linear_num <- - 1.0
 
   let rec curr_node = function
-    | Pstart (node, _) -> node
-    | Pnode (node, _, _, _, _, _) -> node
+    | Pstart (node, _) -> Some node
+    | Pnode (node, _, _, _, _, _) -> Some node
     | Pcall(p1, _, _, _) -> curr_node p1
-    | Pjoin _ -> assert false
+    | Pjoin _ ->
+        None
 
   let exname_opt_compare eo1 eo2 = match eo1, eo2 with
     | None, None -> 0
@@ -306,8 +307,10 @@ end = struct
       | Some pos -> Sil.path_pos_equal (get_path_pos node) pos in
     let path_pos_at_path p =
       try
-        let node = curr_node p in
-        pos_opt <> None && filter node
+        match curr_node p with
+        | Some node ->
+            pos_opt <> None && filter node
+        | None -> false
       with exn when exn_not_timeout exn -> false in
     let position_seen = ref false in
     let inverse_sequence =
@@ -333,12 +336,17 @@ end = struct
   (** return the node visited most, and number of visits, in the longest linear sequence *)
   let repetitions path =
     let map = ref NodeMap.empty in
-    let add_node node =
-      try
-        let n = NodeMap.find node !map in
-        map := NodeMap.add node (n + 1) !map
-      with Not_found ->
-        map := NodeMap.add node 1 !map in
+    let add_node = function
+      | Some node ->
+          begin
+            try
+              let n = NodeMap.find node !map in
+              map := NodeMap.add node (n + 1) !map
+            with Not_found ->
+              map := NodeMap.add node 1 !map
+          end
+      | None ->
+          () in
     iter_longest_sequence (fun level p s exn_opt -> add_node (curr_node p)) None path;
     let max_rep_node = ref (Cfg.Node.dummy ()) in
     let max_rep_num = ref 0 in
@@ -423,51 +431,69 @@ end = struct
         Errlog.lt_description = descr;
         Errlog.lt_node_tags = node_tags } in
     let g level path session exn_opt =
-      let curr_node = curr_node path in
-      let curr_loc = Cfg.Node.get_loc curr_node in
-      match Cfg.Node.get_kind curr_node with
-      | Cfg.Node.Join_node -> () (* omit join nodes from error traces *)
-      | Cfg.Node.Start_node pdesc ->
-          let pname = Cfg.Procdesc.get_proc_name pdesc in
-          let name = Procname.to_string pname in
-          let name_id = Procname.to_filename pname in
-          let descr = "start of procedure " ^ (Procname.to_simplified_string pname) in
-          let node_tags = [(Io_infer.Xml.tag_kind,"procedure_start"); (Io_infer.Xml.tag_name, name); (Io_infer.Xml.tag_name_id, name_id)] in
-          trace := mk_trace_elem level curr_loc descr node_tags :: !trace
-      | Cfg.Node.Prune_node (is_true_branch, if_kind, _) ->
-          let descr = match is_true_branch, if_kind with
-            | true, Sil.Ik_if -> "Taking true branch"
-            | false, Sil.Ik_if -> "Taking false branch"
-            | true, (Sil.Ik_for | Sil.Ik_while | Sil.Ik_dowhile) -> "Loop condition is true. Entering loop body"
-            | false, (Sil.Ik_for | Sil.Ik_while | Sil.Ik_dowhile) -> "Loop condition is false. Leaving loop"
-            | true, Sil.Ik_switch -> "Switch condition is true. Entering switch case"
-            | false, Sil.Ik_switch -> "Switch condition is false. Skipping switch case"
-            | true, (Sil.Ik_bexp | Sil.Ik_land_lor) -> "Condition is true"
-            | false, (Sil.Ik_bexp | Sil.Ik_land_lor) -> "Condition is false" in
-          let node_tags = [(Io_infer.Xml.tag_kind,"condition"); (Io_infer.Xml.tag_branch, if is_true_branch then "true" else "false")] in
-          trace := mk_trace_elem level curr_loc descr node_tags :: !trace
-      | Cfg.Node.Exit_node pdesc ->
-          let pname = Cfg.Procdesc.get_proc_name pdesc in
-          let descr = "return from a call to " ^ (Procname.to_string pname) in
-          let name = Procname.to_string pname in
-          let name_id = Procname.to_filename pname in
-          let node_tags = [(Io_infer.Xml.tag_kind,"procedure_end"); (Io_infer.Xml.tag_name, name); (Io_infer.Xml.tag_name_id, name_id)] in
-          trace := mk_trace_elem level curr_loc descr node_tags :: !trace
-      | _ ->
-          let descr, node_tags =
-            match exn_opt with
-            | None -> "", []
-            | Some exn_name ->
-                let exn_str = Mangled.to_string exn_name in
-                if exn_str = ""
-                then "exception", [(Io_infer.Xml.tag_kind,"exception")]
-                else "exception " ^ exn_str, [(Io_infer.Xml.tag_kind,"exception"); (Io_infer.Xml.tag_name, exn_str)] in
-          let descr =
-            match get_description path with
-            | Some path_descr ->
-                if String.length descr > 0 then descr^" "^path_descr else path_descr
-            | None -> descr in
-          trace := mk_trace_elem level curr_loc descr node_tags :: !trace in
+      match curr_node path with
+      | Some curr_node ->
+          begin
+            let curr_loc = Cfg.Node.get_loc curr_node in
+            match Cfg.Node.get_kind curr_node with
+            | Cfg.Node.Join_node -> () (* omit join nodes from error traces *)
+            | Cfg.Node.Start_node pdesc ->
+                let pname = Cfg.Procdesc.get_proc_name pdesc in
+                let name = Procname.to_string pname in
+                let name_id = Procname.to_filename pname in
+                let descr = "start of procedure " ^ (Procname.to_simplified_string pname) in
+                let node_tags =
+                  [(Io_infer.Xml.tag_kind,"procedure_start");
+                   (Io_infer.Xml.tag_name, name);
+                   (Io_infer.Xml.tag_name_id, name_id)] in
+                trace := mk_trace_elem level curr_loc descr node_tags :: !trace
+            | Cfg.Node.Prune_node (is_true_branch, if_kind, _) ->
+                let descr = match is_true_branch, if_kind with
+                  | true, Sil.Ik_if -> "Taking true branch"
+                  | false, Sil.Ik_if -> "Taking false branch"
+                  | true, (Sil.Ik_for | Sil.Ik_while | Sil.Ik_dowhile) ->
+                      "Loop condition is true. Entering loop body"
+                  | false, (Sil.Ik_for | Sil.Ik_while | Sil.Ik_dowhile) ->
+                      "Loop condition is false. Leaving loop"
+                  | true, Sil.Ik_switch -> "Switch condition is true. Entering switch case"
+                  | false, Sil.Ik_switch -> "Switch condition is false. Skipping switch case"
+                  | true, (Sil.Ik_bexp | Sil.Ik_land_lor) -> "Condition is true"
+                  | false, (Sil.Ik_bexp | Sil.Ik_land_lor) -> "Condition is false" in
+                let node_tags =
+                  [(Io_infer.Xml.tag_kind,"condition");
+                   (Io_infer.Xml.tag_branch, if is_true_branch then "true" else "false")] in
+                trace := mk_trace_elem level curr_loc descr node_tags :: !trace
+            | Cfg.Node.Exit_node pdesc ->
+                let pname = Cfg.Procdesc.get_proc_name pdesc in
+                let descr = "return from a call to " ^ (Procname.to_string pname) in
+                let name = Procname.to_string pname in
+                let name_id = Procname.to_filename pname in
+                let node_tags =
+                  [(Io_infer.Xml.tag_kind,"procedure_end");
+                   (Io_infer.Xml.tag_name, name);
+                   (Io_infer.Xml.tag_name_id, name_id)] in
+                trace := mk_trace_elem level curr_loc descr node_tags :: !trace
+            | _ ->
+                let descr, node_tags =
+                  match exn_opt with
+                  | None -> "", []
+                  | Some exn_name ->
+                      let exn_str = Mangled.to_string exn_name in
+                      if exn_str = ""
+                      then "exception", [(Io_infer.Xml.tag_kind,"exception")]
+                      else
+                        "exception " ^ exn_str,
+                        [(Io_infer.Xml.tag_kind,"exception");
+                         (Io_infer.Xml.tag_name, exn_str)] in
+                let descr =
+                  match get_description path with
+                  | Some path_descr ->
+                      if String.length descr > 0 then descr^" "^path_descr else path_descr
+                  | None -> descr in
+                trace := mk_trace_elem level curr_loc descr node_tags :: !trace
+          end
+      | None ->
+          () in
     iter_longest_sequence g pos_opt path;
     let compare lt1 lt2 =
       let n = int_compare lt1.Errlog.lt_level lt2.Errlog.lt_level in
diff --git a/infer/src/backend/paths.mli b/infer/src/backend/paths.mli
index 36da1747b..213a659d4 100644
--- a/infer/src/backend/paths.mli
+++ b/infer/src/backend/paths.mli
@@ -31,7 +31,7 @@ module Path : sig
   val create_loc_trace : t -> Sil.path_pos option -> Errlog.loc_trace
 
   (** return the current node of the path *)
-  val curr_node : t -> Cfg.node
+  val curr_node : t -> Cfg.node option
 
   (** dump a path *)
   val d : t -> unit
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index d727c6f0d..f266e085d 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -826,8 +826,12 @@ let normalize_params pdesc prop actual_params =
   let prop, args = IList.fold_left norm_arg (prop, []) actual_params in
   (prop, IList.rev args)
 
-let do_error_checks node instr pname pdesc =
-  if !Config.curr_language = Config.Java then PrintfArgs.check_printf_args_ok node instr pname pdesc
+let do_error_checks node_opt instr pname pdesc = match node_opt with
+  | Some node ->
+      if !Config.curr_language = Config.Java then
+        PrintfArgs.check_printf_args_ok node instr pname pdesc
+  | None ->
+      ()
 
 (** Execute [instr] with a symbolic heap [prop].*)
 let rec sym_exec cfg tenv pdesc _instr (_prop: Prop.normal Prop.t) path