Abductive generalisation transformer

[rajdeep87]

Following scenario shows invalid result produced by the abductive generalisation transformer:
Input::
Initial value:: $guard#25 && !(x#phi25 >= 1) && !(-((signed __CPROVER_bitvector[33])x#phi25) >= 1) && $cond#23 && $guard#0 && !$cond#21 && !$guard#24 && $guard#22 && !(-((signed __CPROVER_bitvector[33])x#16) >= 1)

Antecedent clause (statement):: x#phi25 == ($guard#24 ? x#24 : x#22)

Final value:: !(x#22 >= 1) && !(-((signed __CPROVER_bitvector[33])x#22) >= 1)

Variable set:: $cond#21 $cond#23 $guard#0 $guard#22 $guard#24 $guard#25 x#16 x#22 x#24 x#phi25

Output:
Generalization of Initial value:: !(x#22 >= 1) && !(-((signed __CPROVER_bitvector[33])x#22) >= 1)

We want a generalisation of the initial value. But the adductive transformer simply returns the same final value that is passed to the following abductive transformer.
ssa_analyzer(*solver, SSA, implies_exprt(conjunction(final_value), statement), template_generator);

[rajdeep87]

Inferring reason using SAT solver.
get_reason(statement, initial_value, final_value, reason);
Choose a subset of initial_value say v using some heuristic.
We do the following to check if v is the reason:
*solver << implies_exprt(and_expr(statement, conjunction(v)), conjunction(final_value));
result = (*solver)();
if(result == SAT) then v is the reason