Skip to content

Commit d57737a

Browse files
committed
Remove "overflow-typecast-*" expression
1 parent baa45f1 commit d57737a

File tree

1 file changed

+0
-35
lines changed

1 file changed

+0
-35
lines changed

src/solvers/flattening/boolbv_overflow.cpp

Lines changed: 0 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -170,41 +170,6 @@ literalt boolbvt::convert_overflow(const exprt &expr)
170170

171171
return bv_utils.overflow_negate(bv);
172172
}
173-
else if(has_prefix(expr.id_string(), "overflow-typecast-"))
174-
{
175-
std::size_t bits=unsafe_string2unsigned(id2string(expr.id()).substr(18));
176-
INVARIANT(bits != 0, "");
177-
178-
const exprt::operandst &operands=expr.operands();
179-
180-
DATA_INVARIANT(
181-
operands.size() == 1,
182-
"expression " + expr.id_string() + " should have one operand");
183-
184-
const exprt &op=operands[0];
185-
186-
const bvt &bv=convert_bv(op);
187-
188-
INVARIANT(bits < bv.size(), "");
189-
190-
// signed or unsigned?
191-
if(op.type().id()==ID_signedbv)
192-
{
193-
bvt tmp_bv;
194-
for(std::size_t i=bits; i<bv.size(); i++)
195-
tmp_bv.push_back(prop.lxor(bv[bits-1], bv[i]));
196-
197-
return prop.lor(tmp_bv);
198-
}
199-
else
200-
{
201-
bvt tmp_bv;
202-
for(std::size_t i=bits; i<bv.size(); i++)
203-
tmp_bv.push_back(bv[i]);
204-
205-
return prop.lor(tmp_bv);
206-
}
207-
}
208173

209174
return SUB::convert_rest(expr);
210175
}

0 commit comments

Comments
 (0)