diff options
Diffstat (limited to 'Source/VCExpr/Boogie2VCExpr.ssc')
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.ssc | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/Source/VCExpr/Boogie2VCExpr.ssc b/Source/VCExpr/Boogie2VCExpr.ssc index b344c03d..f9f76465 100644 --- a/Source/VCExpr/Boogie2VCExpr.ssc +++ b/Source/VCExpr/Boogie2VCExpr.ssc @@ -416,13 +416,13 @@ namespace Microsoft.Boogie.VCExprAST ///////////////////////////////////////////////////////////////////////////////////
- public override ExtractExpr! VisitExtractExpr(ExtractExpr! node)
+ public override BvExtractExpr! VisitBvExtractExpr(BvExtractExpr! node)
{
- Push(TranslateExtractExpr(node));
+ Push(TranslateBvExtractExpr(node));
return node;
}
- private VCExpr! TranslateExtractExpr(ExtractExpr! node)
+ private VCExpr! TranslateBvExtractExpr(BvExtractExpr! node)
requires node.Start <= node.End; {
VCExpr! bv = Translate(node.Bitvector);
return Gen.BvExtract(bv, ((!)node.Bitvector.Type).BvBits, node.Start, node.End);
|