diff options
| author |  0biha <unknown> | 2014-12-24 20:33:19 +0100 |
|---|---|---|
| committer | 0biha <unknown> | 2014-12-24 20:33:19 +0100 |
| commit | ecf9311b42c5ac54d96a6eb20f4ea3308d470317 (patch) | |
| tree | 524e50642d4e1c9ddadd72fa9824d214ee0b0ef9 /Source/Core/CommandLineOptions.cs | |
| parent | 9a755fa5cd1a93d3b0dbda8d3d58ec1869abbcd3 (diff) | |
Made invariant of class 'CommandLineOptions' robust by changing the design
(made field 'Ai' read-only).
Diffstat (limited to 'Source/Core/CommandLineOptions.cs')
| -rw-r--r-- | Source/Core/CommandLineOptions.cs | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Source/Core/CommandLineOptions.cs b/Source/Core/CommandLineOptions.cs index 503a4d0a..35e1edc9 100644 --- a/Source/Core/CommandLineOptions.cs +++ b/Source/Core/CommandLineOptions.cs @@ -711,7 +711,7 @@ namespace Microsoft.Boogie { public bool J_Intervals = false;
public bool DebugStatistics = false;
}
- public AiFlags/*!*/ Ai = new AiFlags();
+ public readonly AiFlags/*!*/ Ai = new AiFlags();
public class ConcurrentHoudiniOptions
{
|