mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +00:00
Code Activity

refactor: remove unused variable in smt_case_split_queue

Browse source
This commit is contained in:
Murphy Berzish 2017-02-23 15:05:43 -05:00
parent 5107e5cafc
commit 858c754b15
1 changed files with 18 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

46
src/smt/smt_case_split_queue.cpp
View file

@ -1351,35 +1351,25 @@ namespace smt {
p.m_case_split_strategy = CS_ACTIVITY;
}
case_split_queue * baseQueue;
if (p.m_theory_aware_branching) {
// override
baseQueue = alloc(theory_aware_branching_queue, ctx, p);
} else {
switch (p.m_case_split_strategy) {
case CS_ACTIVITY_DELAY_NEW:
baseQueue = alloc(dact_case_split_queue, ctx, p);
break;
case CS_ACTIVITY_WITH_CACHE:
baseQueue = alloc(cact_case_split_queue, ctx, p);
break;
case CS_RELEVANCY:
baseQueue = alloc(rel_case_split_queue, ctx, p);
break;
case CS_RELEVANCY_ACTIVITY:
baseQueue = alloc(rel_act_case_split_queue, ctx, p);
break;
case CS_RELEVANCY_GOAL:
baseQueue = alloc(rel_goal_case_split_queue, ctx, p);
break;
default:
baseQueue = alloc(act_case_split_queue, ctx, p);
break;
if (p.m_theory_aware_branching) {
// override
return alloc(theory_aware_branching_queue, ctx, p);
} else {
switch (p.m_case_split_strategy) {
case CS_ACTIVITY_DELAY_NEW:
return alloc(dact_case_split_queue, ctx, p);
case CS_ACTIVITY_WITH_CACHE:
return alloc(cact_case_split_queue, ctx, p);
case CS_RELEVANCY:
return alloc(rel_case_split_queue, ctx, p);
case CS_RELEVANCY_ACTIVITY:
return alloc(rel_act_case_split_queue, ctx, p);
case CS_RELEVANCY_GOAL:
return alloc(rel_goal_case_split_queue, ctx, p);
default:
return alloc(act_case_split_queue, ctx, p);
}
}
}
return baseQueue;
}
};