diff options
| author |  Michal Moskal <michal@moskal.me> | 2011-09-26 17:30:05 -0700 |
|---|---|---|
| committer | Michal Moskal <michal@moskal.me> | 2011-09-26 17:30:05 -0700 |
| commit | 3925750a1b2145ebd81bea338b33898e61ef10f7 (patch) | |
| tree | 8b3c12cf68036b92246f8c4cfb0b7169ae49258b /Source/VCExpr/SimplifyLikeLineariser.cs | |
| parent | 9dc8e1c990bcb92e7992041f17dd9e0bb88f1b21 (diff) | |
Name the constant used in @MV_state function applications - otherwise we get invalid Z3 files
Diffstat (limited to 'Source/VCExpr/SimplifyLikeLineariser.cs')
| -rw-r--r-- | Source/VCExpr/SimplifyLikeLineariser.cs | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs index c907bd9f..58c6ad7a 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.cs +++ b/Source/VCExpr/SimplifyLikeLineariser.cs @@ -206,6 +206,7 @@ namespace Microsoft.Boogie.VCExprAST { public static string MakeIdPrintable(string s) {
Contract.Requires(s != null);
+ Contract.Requires(s != "");
Contract.Ensures(Contract.Result<string>() != null);
// make sure that no keywords are used as identifiers
switch (s) {
|