Skip to content

Commit 1e4fd71

Browse files
committed
Do not unnecessarily sort guard conjuncts
They are constructed in a consistent order anyway.
1 parent a695814 commit 1e4fd71

File tree

1 file changed

+2
-6
lines changed

1 file changed

+2
-6
lines changed

src/util/guard.cpp

Lines changed: 2 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -95,9 +95,7 @@ guardt &operator -= (guardt &g1, const guardt &g2)
9595
if(g1.id()!=ID_and || g2.id()!=ID_and)
9696
return g1;
9797

98-
sort_and_join(g1);
9998
guardt g2_sorted=g2;
100-
sort_and_join(g2_sorted);
10199

102100
exprt::operandst &op1=g1.operands();
103101
const exprt::operandst &op2=g2_sorted.operands();
@@ -108,10 +106,10 @@ guardt &operator -= (guardt &g1, const guardt &g2)
108106
it2!=op2.end();
109107
++it2)
110108
{
111-
while(it1!=op1.end() && *it1<*it2)
112-
++it1;
113109
if(it1!=op1.end() && *it1==*it2)
114110
it1=op1.erase(it1);
111+
else
112+
break;
115113
}
116114

117115
g1=conjunction(op1);
@@ -145,9 +143,7 @@ guardt &operator |= (guardt &g1, const guardt &g2)
145143
}
146144

147145
// find common prefix
148-
sort_and_join(g1);
149146
guardt g2_sorted=g2;
150-
sort_and_join(g2_sorted);
151147

152148
exprt::operandst &op1=g1.operands();
153149
const exprt::operandst &op2=g2_sorted.operands();

0 commit comments

Comments
 (0)