#include "concretepredicate.h"
#include "model.h"
+#include "execution.h"
+#include "newfuzzer.h"
#include <cmath>
FuncNode::FuncNode(ModelHistory * history) :
inst_id_map_t * inst_id_map = thrd_inst_id_maps[thread_id]->back();
Predicate * curr_pred = get_predicate_tree_position(tid);
+ NewFuzzer * fuzzer = (NewFuzzer *)model->get_execution()->getFuzzer();
+ Predicate * selected_branch = fuzzer->get_selected_child_branch(tid);
+
+ bool amended;
while (true) {
FuncInst * next_inst = get_inst(next_act);
next_inst->set_associated_read(tid, recursion_depth, this_marker, next_act->get_reads_from_value());
// A branch with unset predicate expression is detected
if (!branch_found && unset_predicate != NULL) {
- bool amended = amend_predicate_expr(curr_pred, next_inst, next_act);
+ amended = amend_predicate_expr(curr_pred, next_inst, next_act);
if (amended)
continue;
else {
add_predicate_to_trace(tid, curr_pred);
break;
}
+
+ // A check
+ if (selected_branch != NULL && !amended)
+ ASSERT(selected_branch == curr_pred);
}
/* Given curr_pred and next_inst, find the branch following curr_pred that