+ thrd_loc_inst_maps[thread_id]->pop_back();
+ thrd_inst_id_maps[thread_id]->pop_back();
+ thrd_inst_pred_maps[thread_id]->pop_back();
+ } else {
+ thrd_loc_inst_maps[thread_id]->back()->reset();
+ thrd_inst_id_maps[thread_id]->back()->reset();
+ thrd_inst_pred_maps[thread_id]->back()->reset();
+ }
+}
+
+void FuncNode::init_predicate_tree_data_structure(thread_id_t tid)
+{
+ int thread_id = id_to_int(tid);
+ int old_size = thrd_predicate_tree_position.size();
+
+ if (old_size < thread_id + 1) {
+ thrd_predicate_tree_position.resize(thread_id + 1);
+ thrd_predicate_trace.resize(thread_id + 1);
+
+ for (int i = old_size;i < thread_id + 1;i++) {
+ thrd_predicate_tree_position[i] = new ModelVector<Predicate *>();
+ thrd_predicate_trace[i] = new ModelVector<predicate_trace_t *>();
+ }
+ }
+
+ thrd_predicate_tree_position[thread_id]->push_back(predicate_tree_entry);
+ thrd_predicate_trace[thread_id]->push_back(new predicate_trace_t());
+}
+
+void FuncNode::reset_predicate_tree_data_structure(thread_id_t tid)
+{
+ int thread_id = id_to_int(tid);
+ thrd_predicate_tree_position[thread_id]->pop_back();
+
+ // Free memories allocated in init_predicate_tree_data_structure
+ delete thrd_predicate_trace[thread_id]->back();
+ thrd_predicate_trace[thread_id]->pop_back();