+}
+
+void FuncNode::deep_update(Predicate * curr_pred)
+{
+ FuncInst * func_inst = curr_pred->get_func_inst();
+ if (func_inst != NULL && !func_inst->is_single_location()) {
+ bool has_null_pred = false;
+ PredExprSet * pred_expressions = curr_pred->get_pred_expressions();
+ PredExprSetIter * pred_expr_it = pred_expressions->iterator();
+ while (pred_expr_it->hasNext()) {
+ pred_expr * pred_expression = pred_expr_it->next();
+ if (pred_expression->token == NULLITY) {
+ has_null_pred = true;
+ break;
+ }
+ }
+
+ if (!has_null_pred) {
+// func_inst->print();
+ Predicate * parent = curr_pred->get_parent();
+ curr_pred->add_predicate(NULLITY, NULL, 0);
+
+ Predicate * another_branch = new Predicate(func_inst);
+ another_branch->add_predicate(NULLITY, NULL, 1);
+ parent->add_child(another_branch);
+// another_branch.add_children(i);
+ }
+ }