diff options
| author |  qadeer <unknown> | 2010-04-20 00:07:07 +0000 |
|---|---|---|
| committer | qadeer <unknown> | 2010-04-20 00:07:07 +0000 |
| commit | 052e3794a7a32397a75e51be8913776e62aff315 (patch) | |
| tree | 6057f9efe70a52c748624a18a20ea68466226ae8 /Source/VCExpr | |
| parent | b51c9db20a47aa974d44fbbc8b2b4671b1049bb7 (diff) | |
Fixed bug in translation of select/store arguments that are Boolean
Diffstat (limited to 'Source/VCExpr')
| -rw-r--r-- | Source/VCExpr/SimplifyLikeLineariser.ssc | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/Source/VCExpr/SimplifyLikeLineariser.ssc b/Source/VCExpr/SimplifyLikeLineariser.ssc index d3729ab1..64af05fd 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.ssc +++ b/Source/VCExpr/SimplifyLikeLineariser.ssc @@ -693,21 +693,21 @@ namespace Microsoft.Boogie.VCExprAST }
public bool VisitSelectOp (VCExprNAry! node, LineariserOptions! options) {
- wr.Write("(" + SelectOpName(node) + " ");
- ExprLineariser.Linearise(node[0], options);
- wr.Write(" ");
- ExprLineariser.Linearise(node[1], options);
+ wr.Write("(" + SelectOpName(node));
+ foreach (VCExpr! e in node) {
+ wr.Write(" ");
+ ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
+ }
wr.Write(")");
return true;
}
public bool VisitStoreOp (VCExprNAry! node, LineariserOptions! options) {
- wr.Write("(" + StoreOpName(node) + " ");
- ExprLineariser.Linearise(node[0], options);
- wr.Write(" ");
- ExprLineariser.Linearise(node[1], options);
- wr.Write(" ");
- ExprLineariser.Linearise(node[2], options);
+ wr.Write("(" + StoreOpName(node));
+ foreach (VCExpr! e in node) {
+ wr.Write(" ");
+ ExprLineariser.Linearise(e, options.SetAsTerm(!e.Type.IsBool));
+ }
wr.Write(")");
return true;
}
|