We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent b2fba97 commit d7bb937Copy full SHA for d7bb937
src/analyses/interval_domain.cpp
@@ -82,10 +82,13 @@ void interval_domaint::transform(
82
// of instructions because this is a GOTO.
83
locationt next=from;
84
next++;
85
- if(next==to)
86
- assume(not_exprt(instruction.guard), ns);
87
- else
88
- assume(instruction.guard, ns);
+ if(from->get_target() != next) // If equal then a skip
+ {
+ if(next == to)
+ assume(not_exprt(instruction.guard), ns);
89
+ else
90
+ assume(instruction.guard, ns);
91
+ }
92
}
93
break;
94
0 commit comments