Project

General

Profile

Bug #7760

Infinite loop in theory refinement

Added by Martin Blicha 6 months ago.

Status:
New
Priority:
Normal
Assignee:
-
Start date:
24/08/2018
Due date:
% Done:

0%


Description

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;

Also available in: Atom PDF