diff options
| author |  wuestholz <unknown> | 2015-01-02 22:54:49 +0100 |
|---|---|---|
| committer | wuestholz <unknown> | 2015-01-02 22:54:49 +0100 |
| commit | 96861beb1b7d47bc0b940ff83d5a721d5e67d924 (patch) | |
| tree | 22c527f190d25df6a492d5ad58188e4553ed30d0 /Source/ExecutionEngine/ExecutionEngine.cs | |
| parent | 83ce1429f2897d10e36ecbb49751429674302745 (diff) | |
Minor changes
Diffstat (limited to 'Source/ExecutionEngine/ExecutionEngine.cs')
| -rw-r--r-- | Source/ExecutionEngine/ExecutionEngine.cs | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs index 8187db01..89f9a2c3 100644 --- a/Source/ExecutionEngine/ExecutionEngine.cs +++ b/Source/ExecutionEngine/ExecutionEngine.cs @@ -1247,9 +1247,10 @@ namespace Microsoft.Boogie {
lock (outputs)
{
- for (; nextPrintableIndex < outputs.Count() && outputs[nextPrintableIndex] != null; nextPrintableIndex++)
+ for (; nextPrintableIndex < outputs.Length && outputs[nextPrintableIndex] != null; nextPrintableIndex++)
{
Console.Write(outputs[nextPrintableIndex].ToString());
+ outputs[nextPrintableIndex] = null;
Console.Out.Flush();
}
}
|