A very simple and sound loop handler would be: Chaos all the variables that get modified in the loop (with possible heuristics if a variable can be "hoisted").
Not trivial if used in comparative mode, since we need to compare two "chaoses", but one can imagine heuristics here as well.
This might bring significant performance gains for very simple properties.
A very simple and sound loop handler would be: Chaos all the variables that get modified in the loop (with possible heuristics if a variable can be "hoisted").
Not trivial if used in comparative mode, since we need to compare two "chaoses", but one can imagine heuristics here as well.
This might bring significant performance gains for very simple properties.