summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar qadeer <unknown>2010-04-20 00:07:07 +0000
committerGravatar qadeer <unknown>2010-04-20 00:07:07 +0000
commit052e3794a7a32397a75e51be8913776e62aff315 (patch)
tree6057f9efe70a52c748624a18a20ea68466226ae8
parentb51c9db20a47aa974d44fbbc8b2b4671b1049bb7 (diff)
Fixed bug in translation of select/store arguments that are Boolean
-rw-r--r--Source/VCExpr/SimplifyLikeLineariser.ssc20
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;
}