diff options
| author |  MichalMoskal <unknown> | 2010-08-18 00:54:22 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2010-08-18 00:54:22 +0000 |
| commit | 024e1669cac41a45ba0d825035a25d32a1562a67 (patch) | |
| tree | 09df808ad88aa3977b4997f2b8ef4323e167d365 /Source/VCExpr | |
| parent | a54af4e97ccf24b7bd8802d7411b67bc2b4c5e55 (diff) | |
Fix stack overflow introduced in my previous checkin. Make /typeEncoding:m use separate Z3 type per Boogie type
Diffstat (limited to 'Source/VCExpr')
| -rw-r--r-- | Source/VCExpr/SimplifyLikeLineariser.cs | 5 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprASTVisitors.cs | 6 |
2 files changed, 6 insertions, 5 deletions
diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs index b8a53b9f..84cf0454 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.cs +++ b/Source/VCExpr/SimplifyLikeLineariser.cs @@ -264,10 +264,7 @@ Contract.Ensures(Contract.Result<string>() != null); return TypeToStringHelper(t);
else {
// at this point, only the types U, T, and bitvector types should be left
- if (CommandLineOptions.Clo.TypeEncodingMethod == CommandLineOptions.TypeEncoding.Monomorphic)
- return "U";
- else
- return TypeToStringHelper(t);
+ return TypeToStringHelper(t);
}
}
diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs index 1675a3a7..e87b04ce 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -257,7 +257,11 @@ Contract.Requires(node != null); Result res = StandardResult(node, arg);
- if (node.TypeParamArity == 0) {
+ if (node.TypeParamArity == 0 &&
+ (node.Op == VCExpressionGenerator.AndOp ||
+ node.Op == VCExpressionGenerator.OrOp ||
+ node.Op == VCExpressionGenerator.ImpliesOp))
+ {
Contract.Assert(node.Op != null);
VCExprOp op = node.Op;
|