hifrog

In current version (e.g. f4aaed49) there is bug in theory refinement algorithm. In cases 6 and 7 there is an infinite loop.
The variable in the condition (last) is not modified inside the loop.

case 7 :
// backward with multiple refinement & dependencies
last = exprs.size()-1; {
while (last >= 0){
smtcheck_opensmt2t_cuf decider2(bw,
options.get_unsigned_int_option("type-byte-constraints"),
"backward with multiple refinement & dependencies"
);
decider2.check_ce(exprs, model, refined, weak, last, -1, -1, 1);
}
}
break;