diff --git a/infer/src/IR/cfg.ml b/infer/src/IR/cfg.ml
index e09c0d6c1..01f3d46d0 100644
--- a/infer/src/IR/cfg.ml
+++ b/infer/src/IR/cfg.ml
@@ -632,11 +632,6 @@ module Node = struct
     proc_desc_fold_nodes fold_node acc proc_desc
 
 (*
-  (** Set the proc desc of the node *)
-  let node_set_proc_desc pdesc node =
-    node.nd_proc <- Some pdesc
-
-
   let remove_node cfg node =
     remove_node' (fun node' -> not (equal node node'))
       cfg node
diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml
index 11ccc36ff..12c5713b1 100644
--- a/infer/src/backend/interproc.ml
+++ b/infer/src/backend/interproc.ml
@@ -483,9 +483,7 @@ let do_symbolic_execution handle_exn tenv
   let instrs = Cfg.Node.get_instrs node in
   (* fresh normal vars must be fresh w.r.t. instructions *)
   Ident.update_name_generator (instrs_get_normal_vars instrs);
-  let pset =
-    SymExec.lifted_sym_exec handle_exn tenv pdesc
-      (Paths.PathSet.from_renamed_list [(prop, path)]) node instrs in
+  let pset = SymExec.node handle_exn tenv node (Paths.PathSet.from_renamed_list [(prop, path)]) in
   L.d_strln ".... After Symbolic Execution ....";
   Propset.d prop (Paths.PathSet.to_propset pset);
   L.d_ln (); L.d_ln();
diff --git a/infer/src/backend/modelBuiltins.ml b/infer/src/backend/modelBuiltins.ml
index e08788681..9ab61356c 100644
--- a/infer/src/backend/modelBuiltins.ml
+++ b/infer/src/backend/modelBuiltins.ml
@@ -23,7 +23,7 @@ let execute___builtin_va_arg { Builtin.pdesc; tenv; prop_; path; ret_ids; args;
   match args, ret_ids with
   | [_; _; (lexp3, typ3)], _ ->
       let instr' = Sil.Set (lexp3, typ3, Sil.exp_zero, loc) in
-      sym_exec_generated true tenv pdesc [instr'] [(prop_, path)]
+      SymExec.instrs ~mask_errors:true tenv pdesc [instr'] [(prop_, path)]
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
 let mk_empty_array size =
@@ -57,7 +57,7 @@ let return_result e prop ret_ids =
 (*  Return None if it fails to add the array *)
 let add_array_to_prop pdesc prop_ lexp typ =
   let pname = Cfg.Procdesc.get_proc_name pdesc in
-  let n_lexp, prop = exp_norm_check_arith pname prop_ lexp in
+  let n_lexp, prop = check_arith_norm_exp pname lexp prop_ in
   begin
     try
       let hpred = IList.find (function
@@ -111,8 +111,8 @@ let execute___set_array_size { Builtin.pdesc; prop_; path; ret_ids; args; }
        | None -> []
        | Some (_, prop_a) -> (* Invariant: prop_a has an array pointed to by lexp *)
            let pname = Cfg.Procdesc.get_proc_name pdesc in
-           let n_lexp, prop__ = exp_norm_check_arith pname prop_a lexp in
-           let n_size, prop = exp_norm_check_arith pname prop__ size in
+           let n_lexp, prop__ = check_arith_norm_exp pname lexp prop_a in
+           let n_size, prop = check_arith_norm_exp pname size prop__ in
            let hpred, sigma' = IList.partition (function
                | Sil.Hpointsto(e, _, _) -> Sil.exp_equal e n_lexp
                | _ -> false) (Prop.get_sigma prop) in
@@ -129,7 +129,7 @@ let execute___print_value { Builtin.pdesc; prop_; path; args; }
   L.err "__print_value: ";
   let pname = Cfg.Procdesc.get_proc_name pdesc in
   let do_arg (lexp, _) =
-    let n_lexp, _ = exp_norm_check_arith pname prop_ lexp in
+    let n_lexp, _ = check_arith_norm_exp pname lexp prop_ in
     L.err "%a " (Sil.pp_exp pe_text) n_lexp in
   IList.iter do_arg args;
   L.err "@.";
@@ -181,8 +181,8 @@ let create_type tenv n_lexp typ prop =
       | None -> prop in
   let sil_is_null = Sil.BinOp (Sil.Eq, n_lexp, Sil.exp_zero) in
   let sil_is_nonnull = Sil.UnOp (Sil.LNot, sil_is_null, None) in
-  let null_case = Propset.to_proplist (prune_polarity true sil_is_null prop) in
-  let non_null_case = Propset.to_proplist (prune_polarity true sil_is_nonnull prop_type) in
+  let null_case = Propset.to_proplist (prune ~positive:true sil_is_null prop) in
+  let non_null_case = Propset.to_proplist (prune ~positive:true sil_is_nonnull prop_type) in
   if ((IList.length non_null_case) > 0) && (!Config.footprint) then
     non_null_case
   else if ((IList.length non_null_case) > 0) && (is_undefined_opt prop n_lexp) then
@@ -194,7 +194,7 @@ let execute___get_type_of { Builtin.pdesc; tenv; prop_; path; ret_ids; args; }
   match args with
   | [(lexp, typ)] when IList.length ret_ids <= 1 ->
       let pname = Cfg.Procdesc.get_proc_name pdesc in
-      let n_lexp, prop = exp_norm_check_arith pname prop_ lexp in
+      let n_lexp, prop = check_arith_norm_exp pname lexp prop_ in
       let props = create_type tenv n_lexp typ prop in
       let aux prop =
         begin
@@ -233,8 +233,8 @@ let execute___instanceof_cast ~instof
   match args with
   | [(val1_, typ1); (texp2_, _)] when IList.length ret_ids <= 1 ->
       let pname = Cfg.Procdesc.get_proc_name pdesc in
-      let val1, prop__ = exp_norm_check_arith pname prop_ val1_ in
-      let texp2, prop = exp_norm_check_arith pname prop__ texp2_ in
+      let val1, prop__ = check_arith_norm_exp pname val1_ prop_ in
+      let texp2, prop = check_arith_norm_exp pname texp2_ prop__ in
       let is_cast_to_reference =
         match typ1 with
         | Sil.Tptr (_, Sil.Pk_reference) -> true
@@ -334,7 +334,7 @@ let execute___set_file_attribute { Builtin.pdesc; prop_; path; ret_ids; args; lo
   match args, ret_ids with
   | [(lexp, _)], _ ->
       let pname = Cfg.Procdesc.get_proc_name pdesc in
-      let n_lexp, prop = exp_norm_check_arith pname prop_ lexp in
+      let n_lexp, prop = check_arith_norm_exp pname lexp prop_ in
       set_resource_attribute prop path n_lexp loc Sil.Rfile
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
@@ -344,7 +344,7 @@ let execute___set_lock_attribute { Builtin.pdesc; prop_; path; ret_ids; args; lo
   match args, ret_ids with
   | [(lexp, _)], _ ->
       let pname = Cfg.Procdesc.get_proc_name pdesc in
-      let n_lexp, prop = exp_norm_check_arith pname prop_ lexp in
+      let n_lexp, prop = check_arith_norm_exp pname lexp prop_ in
       set_resource_attribute prop path n_lexp loc Sil.Rlock
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
@@ -356,7 +356,7 @@ let execute___method_set_ignore_attribute
   match args, ret_ids with
   | [_ ; (lexp, _)], _ ->
       let pname = Cfg.Procdesc.get_proc_name pdesc in
-      let n_lexp, prop = exp_norm_check_arith pname prop_ lexp in
+      let n_lexp, prop = check_arith_norm_exp pname lexp prop_ in
       set_resource_attribute prop path n_lexp loc Sil.Rignore
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
@@ -366,7 +366,7 @@ let execute___set_mem_attribute { Builtin.pdesc; prop_; path; ret_ids; args; loc
   match args, ret_ids with
   | [(lexp, _)], _ ->
       let pname = Cfg.Procdesc.get_proc_name pdesc in
-      let n_lexp, prop = exp_norm_check_arith pname prop_ lexp in
+      let n_lexp, prop = check_arith_norm_exp pname lexp prop_ in
       set_resource_attribute prop path n_lexp loc (Sil.Rmemory Sil.Mnew)
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
@@ -377,7 +377,7 @@ let execute___check_untainted
   match args, ret_ids with
   | [(lexp, _)], _ ->
       let caller_pname = Cfg.Procdesc.get_proc_name pdesc in
-      let n_lexp, prop = exp_norm_check_arith caller_pname prop_ lexp in
+      let n_lexp, prop = check_arith_norm_exp caller_pname lexp prop_ in
       [(check_untainted n_lexp caller_pname callee_pname prop, path)]
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
@@ -387,7 +387,7 @@ let execute___get_hidden_field { Builtin.pdesc; prop_; path; ret_ids; args; }
   match args with
   | [(lexp, _)] ->
       let pname = Cfg.Procdesc.get_proc_name pdesc in
-      let n_lexp, prop = exp_norm_check_arith pname prop_ lexp in
+      let n_lexp, prop = check_arith_norm_exp pname lexp prop_ in
       let ret_val = ref None in
       let return_val p = match !ret_val with
         | Some e -> return_result e p ret_ids
@@ -426,8 +426,8 @@ let execute___set_hidden_field { Builtin.pdesc; prop_; path; args; }
   match args with
   | [(lexp1, _); (lexp2, _)] ->
       let pname = Cfg.Procdesc.get_proc_name pdesc in
-      let n_lexp1, prop__ = exp_norm_check_arith pname prop_ lexp1 in
-      let n_lexp2, prop = exp_norm_check_arith pname prop__ lexp2 in
+      let n_lexp1, prop__ = check_arith_norm_exp pname lexp1 prop_ in
+      let n_lexp2, prop = check_arith_norm_exp pname lexp2 prop__ in
       let foot_var = lazy (Sil.Var (Ident.create_fresh Ident.kfootprint)) in
       let filter_fld_hidden (f, _ ) = Ident.fieldname_is_hidden f in
       let has_fld_hidden fsel = IList.exists filter_fld_hidden fsel in
@@ -456,7 +456,7 @@ let execute___set_hidden_field { Builtin.pdesc; prop_; path; args; }
 (* Update the objective-c hidden counter by applying the operation op and the operand delta.*)
 (* Eg. op=+/- delta is an integer *)
 let execute___objc_counter_update
-    suppress_npe_report op delta
+    ~mask_errors op delta
     { Builtin.pdesc; tenv; prop_; path; args; loc; }
   : Builtin.ret_typ =
   match args with
@@ -484,8 +484,7 @@ let execute___objc_counter_update
            loc) in
       let update_counter_instrs =
         [ counter_to_tmp; update_counter; Sil.Remove_temps([tmp], loc) ] in
-      sym_exec_generated
-        suppress_npe_report tenv pdesc update_counter_instrs [(prop_, path)]
+      SymExec.instrs ~mask_errors tenv pdesc update_counter_instrs [(prop_, path)]
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
 (* Given a list of args checks if the first is the flag indicating whether is a call to
@@ -500,12 +499,12 @@ let get_suppress_npe_flag args =
 let execute___objc_retain_impl
     ({ Builtin.prop_; args; ret_ids; } as builtin_args)
   : Builtin.ret_typ =
-  let suppress_npe_report, args' = get_suppress_npe_flag args in
+  let mask_errors, args' = get_suppress_npe_flag args in
   match args' with
   | [(lexp, _)] ->
       let prop = return_result lexp prop_ ret_ids in
       execute___objc_counter_update
-        suppress_npe_report (Sil.PlusA) (Sil.Int.one)
+        ~mask_errors (Sil.PlusA) (Sil.Int.one)
         { builtin_args with Builtin.prop_ = prop; args = args'; }
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
@@ -523,9 +522,9 @@ let execute___objc_release_impl
     ({ Builtin.args; }
      as builtin_args)
   : Builtin.ret_typ =
-  let suppress_npe_flag, args' = get_suppress_npe_flag args in
+  let mask_errors, args' = get_suppress_npe_flag args in
   execute___objc_counter_update
-    suppress_npe_flag Sil.MinusA Sil.Int.one
+    ~mask_errors Sil.MinusA Sil.Int.one
     { builtin_args with Builtin.args = args'; }
 
 let execute___objc_release builtin_args
@@ -547,7 +546,7 @@ let execute___set_autorelease_attribute
       let pname = Cfg.Procdesc.get_proc_name pdesc in
       let prop = return_result lexp prop_ ret_ids in
       if !Config.objc_memory_model_on then
-        let n_lexp, prop = exp_norm_check_arith pname prop lexp in
+        let n_lexp, prop = check_arith_norm_exp pname lexp prop in
         let prop' = Prop.add_or_replace_exp_attribute prop n_lexp Sil.Aautorelease in
         [(prop', path)]
       else execute___no_op prop path
@@ -584,7 +583,7 @@ let execute___release_autorelease_pool
 
 let set_attr pdesc prop path exp attr =
   let pname = Cfg.Procdesc.get_proc_name pdesc in
-  let n_lexp, prop = exp_norm_check_arith pname prop exp in
+  let n_lexp, prop = check_arith_norm_exp pname exp prop in
   [(Prop.add_or_replace_exp_attribute prop n_lexp attr, path)]
 
 (** Set attibute att *)
@@ -643,8 +642,8 @@ let execute___objc_cast { Builtin.pdesc; prop_; path; ret_ids; args; }
   match args with
   | [(val1_, _); (texp2_, _)] when IList.length ret_ids <= 1 ->
       let pname = Cfg.Procdesc.get_proc_name pdesc in
-      let val1, prop__ = exp_norm_check_arith pname prop_ val1_ in
-      let texp2, prop = exp_norm_check_arith pname prop__ texp2_ in
+      let val1, prop__ = check_arith_norm_exp pname val1_ prop_ in
+      let texp2, prop = check_arith_norm_exp pname texp2_ prop__ in
       (try
          let hpred = IList.find (function
              | Sil.Hpointsto(e1, _, _) -> Sil.exp_equal e1 val1
@@ -665,7 +664,7 @@ let execute_abort { Builtin.proc_name; }
 
 let execute_exit { Builtin.prop_; path; }
   : Builtin.ret_typ =
-  execute_diverge prop_ path
+  SymExec.diverge prop_ path
 
 let _execute_free mk loc acc iter =
   match Prop.prop_iter_current iter with
@@ -717,11 +716,11 @@ let execute_free mk { Builtin.pdesc; instr; tenv; prop_; path; args; loc; }
   | [(lexp, typ)] ->
       begin
         let pname = Cfg.Procdesc.get_proc_name pdesc in
-        let n_lexp, prop = exp_norm_check_arith pname prop_ lexp in
+        let n_lexp, prop = check_arith_norm_exp pname lexp prop_ in
         let prop_nonzero = (* case n_lexp!=0 *)
-          Propset.to_proplist (prune_polarity true n_lexp prop) in
+          Propset.to_proplist (prune ~positive:true n_lexp prop) in
         let prop_zero = (* case n_lexp==0 *)
-          Propset.to_proplist (prune_polarity false n_lexp prop) in
+          Propset.to_proplist (prune ~positive:false n_lexp prop) in
         let plist =
           prop_zero @ (* model: if 0 then skip else _execute_free_nonzero *)
           IList.flatten (IList.map (fun p ->
@@ -758,7 +757,7 @@ let execute_alloc mk can_return_null
     | [ret_id] -> ret_id
     | _ -> Ident.create_fresh Ident.kprimed in
   let size_exp', prop =
-    let n_size_exp, prop = exp_norm_check_arith pname prop_ size_exp in
+    let n_size_exp, prop = check_arith_norm_exp pname size_exp prop_ in
     let n_size_exp' = evaluate_char_sizeof n_size_exp in
     Prop.exp_normalize_prop prop n_size_exp', prop in
   let cnt_te = handle_sizeof_exp size_exp' in
@@ -791,7 +790,7 @@ let execute___cxx_typeid ({ Builtin.pdesc; tenv; prop_; args; loc} as r)
        match rest with
        | [(field_exp, _); (lexp, typ)] ->
            let pname = Cfg.Procdesc.get_proc_name pdesc in
-           let n_lexp, prop = exp_norm_check_arith pname prop_ lexp in
+           let n_lexp, prop = check_arith_norm_exp pname lexp prop_ in
            let typ =
              try
                let hpred = IList.find (function
@@ -803,11 +802,11 @@ let execute___cxx_typeid ({ Builtin.pdesc; tenv; prop_; args; loc} as r)
              with Not_found -> typ in
            let typ_string = Sil.typ_to_string typ in
            let set_instr = Sil.Set (field_exp, Sil.Tvoid, Sil.Const (Sil.Cstr typ_string), loc) in
-           sym_exec_generated true tenv pdesc [set_instr] res
+           SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] res
        | _ -> res)
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
-let execute_pthread_create { Builtin.pdesc; tenv; prop_; path; ret_ids; args; loc; }
+let execute_pthread_create ({ Builtin.prop_; path; args; } as builtin_args)
   : Builtin.ret_typ =
   match args with
   | [_; _; start_routine; arg] ->
@@ -822,8 +821,8 @@ let execute_pthread_create { Builtin.pdesc; tenv; prop_; path; ret_ids; args; lo
              match Specs.get_summary (Procname.from_string_c_fun fun_string) with
              | None -> assert false
              | Some callee_summary ->
-                 sym_exec_call
-                   pdesc tenv prop_ path ret_ids [(routine_arg, snd arg)] callee_summary loc
+                 SymExec.proc_call callee_summary
+                   { builtin_args with args = [(routine_arg, snd arg)] }
            end
        | _ ->
            L.d_str "pthread_create: unknown function ";
@@ -834,14 +833,13 @@ let execute_pthread_create { Builtin.pdesc; tenv; prop_; path; ret_ids; args; lo
 let execute_skip { Builtin.prop_; path; } : Builtin.ret_typ =
   [(prop_, path)]
 
-let execute_scan_function skip_n_arguments
-    { Builtin.pdesc; tenv; prop_; path; ret_ids; args; proc_name; loc; }
+let execute_scan_function skip_n_arguments ({ Builtin.args } as call_args)
   : Builtin.ret_typ =
   match args with
   | _ when IList.length args >= skip_n_arguments ->
       let varargs = ref args in
       for _ = 1 to skip_n_arguments do varargs := IList.tl !varargs done;
-      call_unknown_or_scan tenv true pdesc prop_ path ret_ids None !varargs proc_name loc
+      SymExec.unknown_or_scan_call ~is_scan:true None { call_args with args = !varargs }
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
 let execute__unwrap_exception { Builtin.pdesc; prop_; path; ret_ids; args; }
@@ -850,7 +848,7 @@ let execute__unwrap_exception { Builtin.pdesc; prop_; path; ret_ids; args; }
   | [(ret_exn, _)] ->
       begin
         let pname = Cfg.Procdesc.get_proc_name pdesc in
-        let n_ret_exn, prop = exp_norm_check_arith pname prop_ ret_exn in
+        let n_ret_exn, prop = check_arith_norm_exp pname ret_exn prop_ in
         match n_ret_exn with
         | Sil.Const (Sil.Cexn exp) ->
             let prop_with_exn = return_result exp prop ret_ids in
@@ -864,7 +862,7 @@ let execute_return_first_argument { Builtin.pdesc; prop_; path; ret_ids; args; }
   match args with
   | (arg1_, _):: _ ->
       let pname = Cfg.Procdesc.get_proc_name pdesc in
-      let arg1, prop = exp_norm_check_arith pname prop_ arg1_ in
+      let arg1, prop = check_arith_norm_exp pname arg1_ prop_ in
       let prop' = return_result arg1 prop ret_ids in
       [(prop', path)]
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
@@ -874,9 +872,9 @@ let execute___split_get_nth { Builtin.pdesc; prop_; path; ret_ids; args; }
   match args with
   | [(lexp1, _); (lexp2, _); (lexp3, _)] ->
       let pname = Cfg.Procdesc.get_proc_name pdesc in
-      let n_lexp1, prop__ = exp_norm_check_arith pname prop_ lexp1 in
-      let n_lexp2, prop___ = exp_norm_check_arith pname prop__ lexp2 in
-      let n_lexp3, prop = exp_norm_check_arith pname prop___ lexp3 in
+      let n_lexp1, prop__ = check_arith_norm_exp pname lexp1 prop_ in
+      let n_lexp2, prop___ = check_arith_norm_exp pname lexp2 prop__ in
+      let n_lexp3, prop = check_arith_norm_exp pname lexp3 prop___ in
       (match n_lexp1, n_lexp2, n_lexp3 with
        | Sil.Const (Sil.Cstr str1), Sil.Const (Sil.Cstr str2), Sil.Const (Sil.Cint n_sil) ->
            (let n = Sil.Int.to_int n_sil in
@@ -897,7 +895,7 @@ let execute___infer_assume { Builtin.prop_; path; args; }
   | [(lexp, _)] ->
       let prop_assume = Prop.conjoin_eq lexp (Sil.exp_bool true) prop_ in
       if Prover.check_inconsistency prop_assume
-      then execute_diverge prop_assume path
+      then SymExec.diverge prop_assume path
       else [(prop_assume, path)]
   | _ -> raise (Exceptions.Wrong_argument_number __POS__)
 
@@ -916,7 +914,7 @@ let execute___infer_fail { Builtin.pdesc; tenv; prop_; path; args; loc; }
         raise (Exceptions.Wrong_argument_number __POS__) in
   let set_instr =
     Sil.Set (Sil.Lvar Sil.custom_error, Sil.Tvoid, Sil.Const (Sil.Cstr error_str), loc) in
-  sym_exec_generated true tenv pdesc [set_instr] [(prop_, path)]
+  SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] [(prop_, path)]
 
 (* translate builtin assertion failure *)
 let execute___assert_fail { Builtin.pdesc; tenv; prop_; path; args; loc; }
@@ -929,7 +927,7 @@ let execute___assert_fail { Builtin.pdesc; tenv; prop_; path; args; loc; }
         raise (Exceptions.Wrong_argument_number __POS__) in
   let set_instr =
     Sil.Set (Sil.Lvar Sil.custom_error, Sil.Tvoid, Sil.Const (Sil.Cstr error_str), loc) in
-  sym_exec_generated true tenv pdesc [set_instr] [(prop_, path)]
+  SymExec.instrs ~mask_errors:true tenv pdesc [set_instr] [(prop_, path)]
 
 let __assert_fail = Builtin.register
     "__assert_fail" execute___assert_fail
@@ -1129,7 +1127,7 @@ let execute_objc_alloc_no_fail
   let ptr_typ = Sil.Tptr (typ, Sil.Pk_pointer) in
   let sizeof_typ = Sil.Sizeof (typ, Sil.Subtype.exact) in
   let alloc_instr = Sil.Call (ret_ids, alloc_fun, [sizeof_typ, ptr_typ], loc, Sil.cf_default) in
-  sym_exec_generated false tenv pdesc [alloc_instr] symb_state
+  SymExec.instrs tenv pdesc [alloc_instr] symb_state
 
 let execute_objc_NSArray_alloc_no_fail
     ({ Builtin.tenv; } as builtin_args) symb_state =
@@ -1140,12 +1138,12 @@ let execute_objc_NSArray_alloc_no_fail
 
 let execute_NSArray_arrayWithObjects_count builtin_args =
   let n_formals = 1 in
-  let res = sym_exe_check_variadic_sentinel ~fails_on_nil: true n_formals (0,1) builtin_args in
+  let res = SymExec.check_variadic_sentinel ~fails_on_nil: true n_formals (0,1) builtin_args in
   execute_objc_NSArray_alloc_no_fail builtin_args res
 
 let execute_NSArray_arrayWithObjects builtin_args =
   let n_formals = 1 in
-  let res = sym_exe_check_variadic_sentinel n_formals (0,1) builtin_args in
+  let res = SymExec.check_variadic_sentinel n_formals (0,1) builtin_args in
   execute_objc_NSArray_alloc_no_fail builtin_args res
 
 let _ =
@@ -1172,8 +1170,7 @@ let execute_objc_NSDictionary_alloc_no_fail
 
 let execute___objc_dictionary_literal builtin_args =
   let n_formals = 1 in
-  let res' =
-    sym_exe_check_variadic_sentinel ~fails_on_nil: true n_formals (0,1) builtin_args in
+  let res' = SymExec.check_variadic_sentinel ~fails_on_nil: true n_formals (0,1) builtin_args in
   execute_objc_NSDictionary_alloc_no_fail res' builtin_args
 
 let __objc_dictionary_literal =
diff --git a/infer/src/backend/symExec.ml b/infer/src/backend/symExec.ml
index 4f9114c24..893c530d8 100644
--- a/infer/src/backend/symExec.ml
+++ b/infer/src/backend/symExec.ml
@@ -268,7 +268,7 @@ let rec execute_nullify_se = function
 
 (** Do pruning for conditional [if (e1 != e2) ] if [positive] is true
     and [(if (e1 == e2)] if [positive] is false *)
-let prune_ne positive e1 e2 prop =
+let prune_ne ~positive e1 e2 prop =
   let is_inconsistent =
     if positive then Prover.check_equal prop e1 e2
     else Prover.check_disequal prop e1 e2 in
@@ -283,7 +283,7 @@ let prune_ne positive e1 e2 prop =
     true and "if (!([e1] CMP [e2]))" if [positive] is false, where CMP
     is "<" if [is_strict] is true and "<=" if [is_strict] is false.
 *)
-let prune_ineq ~is_strict positive prop e1 e2 =
+let prune_ineq ~is_strict ~positive prop e1 e2 =
   if Sil.exp_equal e1 e2 then
     if (positive && not is_strict) || (not positive && is_strict) then
       Propset.singleton prop
@@ -308,10 +308,10 @@ let prune_ineq ~is_strict positive prop e1 e2 =
       let prop_with_ineq = Prop.conjoin_eq ~footprint prune_cond Sil.exp_one prop in
       Propset.singleton prop_with_ineq
 
-let rec prune_polarity positive condition prop =
+let rec prune ~positive condition prop =
   match condition with
   | Sil.Var _ | Sil.Lvar _ ->
-      prune_ne positive condition Sil.exp_zero prop
+      prune_ne ~positive condition Sil.exp_zero prop
   | Sil.Const (Sil.Cint i) when Sil.Int.iszero i ->
       if positive then Propset.empty else Propset.singleton prop
   | Sil.Const (Sil.Cint _) | Sil.Sizeof _ | Sil.Const (Sil.Cstr _) | Sil.Const (Sil.Cclass _) ->
@@ -319,45 +319,45 @@ let rec prune_polarity positive condition prop =
   | Sil.Const _ ->
       assert false
   | Sil.Cast (_, condition') ->
-      prune_polarity positive condition' prop
+      prune ~positive condition' prop
   | Sil.UnOp (Sil.LNot, condition', _) ->
-      prune_polarity (not positive) condition' prop
+      prune ~positive:(not positive) condition' prop
   | Sil.UnOp _ ->
       assert false
   | Sil.BinOp (Sil.Eq, e, Sil.Const (Sil.Cint i))
   | Sil.BinOp (Sil.Eq, Sil.Const (Sil.Cint i), e) when Sil.Int.iszero i && not (Sil.Int.isnull i) ->
-      prune_polarity (not positive) e prop
+      prune ~positive:(not positive) e prop
   | Sil.BinOp (Sil.Eq, e1, e2) ->
-      prune_ne (not positive) e1 e2 prop
+      prune_ne ~positive:(not positive) e1 e2 prop
   | Sil.BinOp (Sil.Ne, e, Sil.Const (Sil.Cint i))
   | Sil.BinOp (Sil.Ne, Sil.Const (Sil.Cint i), e) when Sil.Int.iszero i && not (Sil.Int.isnull i) ->
-      prune_polarity positive e prop
+      prune ~positive e prop
   | Sil.BinOp (Sil.Ne, e1, e2) ->
-      prune_ne positive e1 e2 prop
+      prune_ne ~positive e1 e2 prop
   | Sil.BinOp (Sil.Ge, e2, e1) | Sil.BinOp (Sil.Le, e1, e2) ->
-      prune_ineq ~is_strict:false positive prop e1 e2
+      prune_ineq ~is_strict:false ~positive prop e1 e2
   | Sil.BinOp (Sil.Gt, e2, e1) | Sil.BinOp (Sil.Lt, e1, e2) ->
-      prune_ineq ~is_strict:true positive prop e1 e2
+      prune_ineq ~is_strict:true ~positive prop e1 e2
   | Sil.BinOp (Sil.LAnd, condition1, condition2) ->
-      let pruner = if positive then prune_polarity_inter else prune_polarity_union in
-      pruner positive condition1 condition2 prop
+      let pruner = if positive then prune_inter else prune_union in
+      pruner ~positive condition1 condition2 prop
   | Sil.BinOp (Sil.LOr, condition1, condition2) ->
-      let pruner = if positive then prune_polarity_union else prune_polarity_inter in
-      pruner positive condition1 condition2 prop
+      let pruner = if positive then prune_union else prune_inter in
+      pruner ~positive condition1 condition2 prop
   | Sil.BinOp _ | Sil.Lfield _ | Sil.Lindex _ ->
-      prune_ne positive condition Sil.exp_zero prop
+      prune_ne ~positive condition Sil.exp_zero prop
 
-and prune_polarity_inter positive condition1 condition2 prop =
+and prune_inter ~positive condition1 condition2 prop =
   let res = ref Propset.empty in
-  let pset1 = prune_polarity positive condition1 prop in
+  let pset1 = prune ~positive condition1 prop in
   let do_p p =
-    res := Propset.union (prune_polarity positive condition2 p) !res in
+    res := Propset.union (prune ~positive condition2 p) !res in
   Propset.iter do_p pset1;
   !res
 
-and prune_polarity_union positive condition1 condition2 prop =
-  let pset1 = prune_polarity positive condition1 prop in
-  let pset2 = prune_polarity positive condition2 prop in
+and prune_union ~positive condition1 condition2 prop =
+  let pset1 = prune ~positive condition1 prop in
+  let pset2 = prune ~positive condition2 prop in
   Propset.union pset1 pset2
 
 let dangerous_functions =
@@ -407,7 +407,7 @@ let check_constant_string_dereference lexp =
   | _ -> None
 
 (** Normalize an expression and check for arithmetic problems *)
-let exp_norm_check_arith pname prop exp =
+let check_arith_norm_exp pname exp prop =
   match Prop.find_arithmetic_problem (State.get_path_pos ()) prop exp with
   | Some (Prop.Div0 div), prop' ->
       let desc = Errdesc.explain_divide_by_zero div (State.get_node ()) (State.get_loc ()) in
@@ -774,7 +774,7 @@ let handle_objc_method_call actual_pars actual_params pre tenv ret_ids pdesc cal
     if !Config.footprint && not is_undef then
       let res_null = (* returns: (objc_null(res) /\ receiver=0) or an empty list of results *)
         let pre_with_attr_or_null = add_objc_null_attribute_or_nullify_result pre in
-        let propset = prune_ne false receiver Sil.exp_zero pre_with_attr_or_null in
+        let propset = prune_ne ~positive:false receiver Sil.exp_zero pre_with_attr_or_null in
         if Propset.is_empty propset then []
         else
           let prop = IList.hd (Propset.to_proplist propset) in
@@ -785,7 +785,7 @@ let handle_objc_method_call actual_pars actual_params pre tenv ret_ids pdesc cal
 
 let normalize_params pdesc prop actual_params =
   let norm_arg (p, args) (e, t) =
-    let e', p' = exp_norm_check_arith pdesc p e in
+    let e', p' = check_arith_norm_exp pdesc e p in
     (p', (e', t) :: args) in
   let prop, args = IList.fold_left norm_arg (prop, []) actual_params in
   (prop, IList.rev args)
@@ -899,7 +899,7 @@ let execute_letderef ?(report_deref_errors=true) pname pdesc tenv id rhs_exp typ
            should change the implementation here. *)
         assert false in
   try
-    let n_rhs_exp, prop = exp_norm_check_arith pname prop_ rhs_exp in
+    let n_rhs_exp, prop = check_arith_norm_exp pname rhs_exp prop_ in
     let n_rhs_exp' = Prop.exp_collapse_consecutive_indices_prop typ n_rhs_exp in
     match check_constant_string_dereference n_rhs_exp' with
     | Some value ->
@@ -946,8 +946,8 @@ let execute_set ?(report_deref_errors=true) pname pdesc tenv lhs_exp typ rhs_exp
     | None -> update acc_in ([],[])
     | Some pred_insts -> IList.fold_left update acc_in pred_insts in
   try
-    let n_lhs_exp, prop_' = exp_norm_check_arith pname prop_ lhs_exp in
-    let n_rhs_exp, prop = exp_norm_check_arith pname prop_' rhs_exp in
+    let n_lhs_exp, prop_' = check_arith_norm_exp pname lhs_exp prop_ in
+    let n_rhs_exp, prop = check_arith_norm_exp pname rhs_exp prop_' in
     let prop = Prop.replace_objc_null prop n_lhs_exp n_rhs_exp in
     let n_lhs_exp' = Prop.exp_collapse_consecutive_indices_prop typ n_lhs_exp in
     let iter_list = Rearrange.rearrange ~report_deref_errors pdesc tenv n_lhs_exp' typ prop loc in
@@ -965,20 +965,6 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
   SymOp.pay(); (* pay one symop *)
   let ret_old_path pl = (* return the old path unchanged *)
     IList.map (fun p -> (p, path)) pl in
-  let skip_call prop path callee_pname loc ret_ids ret_typ_opt actual_args =
-    let exn = Exceptions.Skip_function (Localise.desc_skip_function callee_pname) in
-    Reporting.log_info current_pname exn;
-    L.d_strln
-      ("Undefined function " ^ Procname.to_string callee_pname
-       ^ ", returning undefined value.");
-    (match Specs.get_summary current_pname with
-     | None -> ()
-     | Some summary ->
-         Specs.CallStats.trace
-           summary.Specs.stats.Specs.call_stats callee_pname loc
-           (Specs.CallStats.CR_skip) !Config.footprint);
-    call_unknown_or_scan
-      tenv false current_pdesc prop path ret_ids ret_typ_opt actual_args callee_pname loc in
   let instr = match _instr with
     | Sil.Call (ret, exp, par, loc, call_flags) ->
         let exp' = Prop.exp_normalize_prop prop_ exp in
@@ -992,6 +978,23 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
               Sil.Call (ret, exp', par, loc, call_flags) in
         instr'
     | _ -> _instr in
+  let skip_call prop path callee_pname loc ret_ids ret_typ_opt actual_args =
+    let exn = Exceptions.Skip_function (Localise.desc_skip_function callee_pname) in
+    Reporting.log_info current_pname exn;
+    L.d_strln
+      ("Undefined function " ^ Procname.to_string callee_pname
+       ^ ", returning undefined value.");
+    (match Specs.get_summary current_pname with
+     | None -> ()
+     | Some summary ->
+         Specs.CallStats.trace
+           summary.Specs.stats.Specs.call_stats callee_pname loc
+           (Specs.CallStats.CR_skip) !Config.footprint);
+    unknown_or_scan_call ~is_scan:false ret_typ_opt Builtin.{
+        pdesc= current_pdesc; instr; tenv; prop_= prop; path; ret_ids; args= actual_args;
+        proc_name= callee_pname; loc; } in
+  let call_args prop_ proc_name args ret_ids loc = {
+    Builtin.pdesc = current_pdesc; instr; tenv; prop_; path; ret_ids; args; proc_name; loc; } in
   match instr with
   | Sil.Letderef (id, rhs_exp, typ, loc) ->
       execute_letderef current_pname current_pdesc tenv id rhs_exp typ loc prop_
@@ -1049,23 +1052,12 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
       if not !Config.report_runtime_exceptions then
         check_already_dereferenced current_pname cond prop__;
       check_condition_always_true_false ();
-      let n_cond, prop = exp_norm_check_arith current_pname prop__ cond in
-      ret_old_path (Propset.to_proplist (prune_polarity true n_cond prop))
+      let n_cond, prop = check_arith_norm_exp current_pname cond prop__ in
+      ret_old_path (Propset.to_proplist (prune ~positive:true n_cond prop))
   | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), args, loc, _)
     when Builtin.is_registered callee_pname ->
       let sym_exe_builtin = Builtin.get callee_pname in
-      sym_exe_builtin
-        {
-          pdesc = current_pdesc;
-          instr;
-          tenv;
-          prop_;
-          path;
-          ret_ids;
-          args;
-          proc_name = callee_pname;
-          loc;
-        }
+      sym_exe_builtin (call_args prop_ callee_pname args ret_ids loc)
   | Sil.Call (ret_ids,
               Sil.Const (Sil.Cfun ((Procname.Java callee_pname_java) as callee_pname)),
               actual_params, loc, call_flags)
@@ -1087,7 +1079,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
         | Some summary when call_should_be_skipped resolved_pname summary ->
             exec_skip_call resolved_pname summary.Specs.attributes.ProcAttributes.ret_type
         | Some summary ->
-            sym_exec_call current_pdesc tenv norm_prop path ret_ids norm_args summary loc
+            proc_call summary (call_args prop_ callee_pname norm_args ret_ids loc)
       end
 
   | Sil.Call (ret_ids,
@@ -1118,7 +1110,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
         | Some summary when call_should_be_skipped pname summary ->
             exec_skip_call summary.Specs.attributes.ProcAttributes.ret_type
         | Some summary ->
-            sym_exec_call current_pdesc tenv norm_prop path ret_ids url_handled_args summary loc in
+            proc_call summary (call_args norm_prop pname url_handled_args ret_ids loc) in
       IList.fold_left (fun acc pname -> exec_one_pname pname @ acc) [] resolved_pnames
 
   | Sil.Call (ret_ids, Sil.Const (Sil.Cfun callee_pname), actual_params, loc, call_flags) ->
@@ -1136,17 +1128,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
       let ret_typ_opt = Option.map Cfg.Procdesc.get_ret_type callee_pdesc_opt in
       let sentinel_result =
         if !Config.curr_language = Config.C_CPP then
-          sym_exe_check_variadic_sentinel_if_present
-            { Builtin.pdesc = current_pdesc;
-              instr;
-              tenv;
-              prop_ = prop_r;
-              path;
-              ret_ids;
-              args = actual_params;
-              proc_name = callee_pname;
-              loc;
-            }
+          check_variadic_sentinel_if_present
+            (call_args prop_r callee_pname actual_params ret_ids loc)
         else [(prop_r, path)] in
       let do_call (prop, path) =
         let attrs_opt = Option.map Cfg.Procdesc.get_attributes callee_pdesc_opt in
@@ -1170,8 +1153,8 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
           | None ->
               skip_call prop path resolved_pname loc ret_ids ret_typ_opt n_actual_params
         else
-          sym_exec_call
-            current_pdesc tenv prop path ret_ids n_actual_params (Option.get summary) loc in
+          proc_call (Option.get summary)
+            (call_args prop resolved_pname n_actual_params ret_ids loc) in
       IList.flatten (IList.map do_call sentinel_result)
   | Sil.Call (ret_ids, fun_exp, actual_params, loc, call_flags) -> (** Call via function pointer *)
       let (prop_r, n_actual_params) = normalize_params current_pname prop_ actual_params in
@@ -1181,13 +1164,14 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
       if call_flags.Sil.cf_noreturn then begin
         L.d_str "Unknown function pointer with noreturn attribute ";
         Sil.d_exp fun_exp; L.d_strln ", diverging.";
-        execute_diverge prop_r path
+        diverge prop_r path
       end else begin
         L.d_str "Unknown function pointer "; Sil.d_exp fun_exp;
         L.d_strln ", returning undefined value.";
         let callee_pname = Procname.from_string_c_fun "__function_pointer__" in
-        call_unknown_or_scan
-          tenv false current_pdesc prop_r path ret_ids None n_actual_params callee_pname loc
+        unknown_or_scan_call ~is_scan:false None Builtin.{
+            pdesc= current_pdesc; instr; tenv; prop_= prop_r; path; ret_ids; args= n_actual_params;
+            proc_name= callee_pname; loc; }
       end
   | Sil.Nullify (pvar, _, deallocate) ->
       begin
@@ -1234,7 +1218,7 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
   | Sil.Stackop _ -> (* this should be handled at the propset level *)
       assert false
   | Sil.Goto_node (node_e, _) ->
-      let n_node_e, prop = exp_norm_check_arith current_pname prop_ node_e in
+      let n_node_e, prop = check_arith_norm_exp current_pname node_e prop_ in
       begin
         match n_node_e with
         | Sil.Const (Sil.Cint i) ->
@@ -1245,13 +1229,13 @@ let rec sym_exec tenv current_pdesc _instr (prop_: Prop.normal Prop.t) path
                   are set to the possible targets by the front-end *)
             [(prop, path)]
       end
-and execute_diverge prop path =
+and diverge prop path =
   State.add_diverging_states (Paths.PathSet.from_renamed_list [(prop, path)]); (* diverge *)
   []
 
-(** Like sym_exec but for generated instructions.
-    If errors occur and [mask_errors] is false, just treat as skip.*)
-and sym_exec_generated mask_errors tenv pdesc instrs ppl =
+(** Symbolic execution of a sequence of instructions.
+    If errors occur and [mask_errors] is true, just treat as skip. *)
+and instrs ?(mask_errors=false) tenv pdesc instrs ppl =
   let exe_instr instr (p, path) =
     L.d_str "Executing Generated Instruction "; Sil.d_instr instr; L.d_ln ();
     try sym_exec tenv pdesc instr p path
@@ -1372,8 +1356,9 @@ and check_untainted exp caller_pname callee_pname prop =
       else prop
 
 (** execute a call for an unknown or scan function *)
-and call_unknown_or_scan tenv is_scan pdesc pre path
-    ret_ids ret_type_option actual_pars callee_pname loc =
+and unknown_or_scan_call ~is_scan ret_type_option
+    { Builtin.tenv; pdesc; prop_= pre; path; ret_ids;
+      args= actual_pars; proc_name= callee_pname; loc; } =
   let remove_file_attribute prop =
     let do_exp p (e, _) =
       let do_attribute q = function
@@ -1427,7 +1412,7 @@ and call_unknown_or_scan tenv is_scan pdesc pre path
     let path_pos = State.get_path_pos () in
     [(Prop.mark_vars_as_undefined pre_final exps_to_mark callee_pname loc path_pos, path)]
 
-and sym_exe_check_variadic_sentinel
+and check_variadic_sentinel
     ?(fails_on_nil = false) n_formals  (sentinel, null_pos)
     { Builtin.pdesc; tenv; prop_; path; args; proc_name; loc; }
   =
@@ -1450,7 +1435,7 @@ and sym_exe_check_variadic_sentinel
     let tmp_id_deref = Ident.create_fresh Ident.kprimed in
     let letderef = Sil.Letderef (tmp_id_deref, lexp, typ, loc) in
     try
-      sym_exec_generated false tenv pdesc [letderef] result
+      instrs tenv pdesc [letderef] result
     with e when exn_not_failure e ->
       if not fails_on_nil then
         let deref_str = Localise.deref_str_nil_argument_in_variadic_method proc_name nargs i in
@@ -1464,7 +1449,7 @@ and sym_exe_check_variadic_sentinel
   (* error on the first premature nil argument *)
   IList.fold_left check_allocated [(prop_, path)] non_terminal_argsi
 
-and sym_exe_check_variadic_sentinel_if_present
+and check_variadic_sentinel_if_present
     ({ Builtin.prop_; path; proc_name; } as builtin_args) =
   match Specs.proc_resolve_attributes proc_name with
   | None ->
@@ -1475,7 +1460,7 @@ and sym_exe_check_variadic_sentinel_if_present
       | None -> [(prop_, path)]
       | Some sentinel_arg ->
           let formals = callee_attributes.ProcAttributes.formals in
-          sym_exe_check_variadic_sentinel (IList.length formals) sentinel_arg builtin_args
+          check_variadic_sentinel (IList.length formals) sentinel_arg builtin_args
 
 and sym_exec_objc_getter field_name ret_typ_opt tenv ret_ids pdesc pname loc args prop =
   L.d_strln ("No custom getter found. Executing the ObjC builtin getter with ivar "^
@@ -1525,7 +1510,7 @@ and sym_exec_objc_accessor property_accesor ret_typ_opt tenv ret_ids pdesc _ loc
   |> IList.map (fun p -> (p, path))
 
 (** Perform symbolic execution for a function call *)
-and sym_exec_call pdesc tenv pre path ret_ids actual_pars summary loc =
+and proc_call summary {Builtin.pdesc; tenv; prop_= pre; path; ret_ids; args= actual_pars; loc; } =
   let caller_pname = Cfg.Procdesc.get_proc_name pdesc in
   let callee_pname = Specs.get_proc_name summary in
   let ret_typ = Specs.get_ret_type summary in
@@ -1663,9 +1648,8 @@ and sym_exec_wrapper handle_exn tenv pdesc instr ((prop: Prop.normal Prop.t), pa
 
 (** {2 Lifted Abstract Transfer Functions} *)
 
-let lifted_sym_exec
-    handle_exn tenv pdesc (pset : Paths.PathSet.t) node (instrs : Sil.instr list)
-  : Paths.PathSet.t =
+let node handle_exn tenv node (pset : Paths.PathSet.t) : Paths.PathSet.t =
+  let pdesc = Cfg.Node.get_proc_desc node in
   let pname = Cfg.Procdesc.get_proc_name pdesc in
   let exe_instr_prop instr p tr (pset1: Paths.PathSet.t) =
     let pset2 =
@@ -1702,6 +1686,7 @@ let lifted_sym_exec
         let pset' = Paths.PathSet.fold (exe_instr_prop instr) pset Paths.PathSet.empty in
         (pset', stack) in
   let stack = [] in
+  let instrs = Cfg.Node.get_instrs node in
   let pset', stack' = IList.fold_left exe_instr_pset (pset, stack) instrs in
   if stack' != [] then assert false; (* final stack must be empty *)
   pset'
diff --git a/infer/src/backend/symExec.mli b/infer/src/backend/symExec.mli
index eb5e416ce..233df6eff 100644
--- a/infer/src/backend/symExec.mli
+++ b/infer/src/backend/symExec.mli
@@ -12,47 +12,38 @@
 
 exception Cannot_convert_string_to_typ of string
 
-val lookup_java_typ_from_string : Tenv.t -> string -> Sil.typ
 (** Lookup Java types by name. May raise [Cannot_convert_string_to_typ]. *)
+val lookup_java_typ_from_string : Tenv.t -> string -> Sil.typ
 
-val resolve_method : Tenv.t -> Typename.t -> Procname.t -> Procname.t
-(** OO method resolution: given a class name and a method name, climb the class hierarchy to find
-    the procname that the method name will actually resolve to at runtime. For example, if we have a
-    procname like Foo.toString() and Foo does not override toString(), we must resolve the call to
-    toString(). We will end up with Super.toString() where Super is some superclass of Foo. *)
+(** Symbolic execution of the instructions of a node, lifted to sets of propositions. *)
+val node : (exn -> unit) -> Tenv.t -> Cfg.Node.t -> Paths.PathSet.t -> Paths.PathSet.t
 
-val prune_polarity : bool -> Sil.exp -> Prop.normal Prop.t -> Propset.t
+(** Symbolic execution of a sequence of instructions.
+    If errors occur and [mask_errors] is true, just treat as skip. *)
+val instrs :
+  ?mask_errors:bool -> Tenv.t -> Cfg.Procdesc.t -> Sil.instr list ->
+  (Prop.normal Prop.t * Paths.Path.t) list -> (Prop.normal Prop.t * Paths.Path.t) list
 
-val exp_norm_check_arith :
-  Procname.t -> Prop.normal Prop.t -> Sil.exp -> Sil.exp * Prop.normal Prop.t
-(** Normalize an expression and check for arithmetic problems *)
+(** Symbolic execution of the divergent pure computation. *)
+val diverge : Prop.normal Prop.t -> Paths.Path.t -> (Prop.normal Prop.t * Paths.Path.t) list
 
-val execute_diverge :
-  Prop.normal Prop.t -> Paths.Path.t -> (Prop.normal Prop.t * Paths.Path.t) list
+val proc_call : Specs.summary -> Builtin.t
 
-val sym_exec_generated :
-  bool -> Tenv.t -> Cfg.Procdesc.t -> Sil.instr list ->
-  (Prop.normal Prop.t * Paths.Path.t) list -> (Prop.normal Prop.t * Paths.Path.t) list
-(** Execute generated instructions from a symbolic heap.
-    If errors occur and [mask_errors] is false, just treat as skip.*)
+val unknown_or_scan_call : is_scan:bool -> Sil.typ option -> Builtin.t
 
-val sym_exe_check_variadic_sentinel :
-  ?fails_on_nil:bool -> int -> int * int -> Builtin.args ->
-  (Prop.normal Prop.t * Paths.Path.t) list
+val check_variadic_sentinel : ?fails_on_nil:bool -> int -> int * int -> Builtin.t
 
 val check_untainted :
   Sil.exp -> Procname.t -> Procname.t -> Prop.normal Prop.t -> Prop.normal Prop.t
 
-val call_unknown_or_scan :
-  Tenv.t -> bool -> Cfg.Procdesc.t -> Prop.normal Prop.t -> Paths.Path.t -> Ident.t list ->
-  Sil.typ option -> (Sil.exp * Sil.typ) list -> Procname.t -> Location.t ->
-  (Prop.normal Prop.t * Paths.Path.t) list
+(** Check for arithmetic problems and normalize an expression. *)
+val check_arith_norm_exp :
+  Procname.t -> Sil.exp -> Prop.normal Prop.t -> Sil.exp * Prop.normal Prop.t
 
-val sym_exec_call :
-  Cfg.Procdesc.t -> Tenv.t -> Prop.normal Prop.t -> Paths.Path.t -> Ident.t list ->
-  (Sil.exp * Sil.typ) list -> Specs.summary -> Location.t ->
-  (Prop.normal Prop.t * Paths.Path.t) list
+val prune : positive:bool -> Sil.exp -> Prop.normal Prop.t -> Propset.t
 
-val lifted_sym_exec : (exn -> unit) -> Tenv.t -> Cfg.Procdesc.t ->
-  Paths.PathSet.t -> Cfg.Node.t -> Sil.instr list -> Paths.PathSet.t
-(** symbolic execution on the level of sets of propositions *)
+(** OO method resolution: given a class name and a method name, climb the class hierarchy to find
+    the procname that the method name will actually resolve to at runtime. For example, if we have a
+    procname like Foo.toString() and Foo does not override toString(), we must resolve the call to
+    toString(). We will end up with Super.toString() where Super is some superclass of Foo. *)
+val resolve_method : Tenv.t -> Typename.t -> Procname.t -> Procname.t