summaryrefslogtreecommitdiff
path: root/Source/ExecutionEngine
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2014-11-02 15:49:18 +0100
committerGravatar wuestholz <unknown>2014-11-02 15:49:18 +0100
commit5964ffcfd89533b83b4b381b894194c76b94c84f (patch)
tree155c78b8e46ea76649ccb690e3e06dc83a09b402 /Source/ExecutionEngine
parent5edb0b7cdaeae035968945cfda687c2ba1d7967a (diff)
Fixed minor issue.
Diffstat (limited to 'Source/ExecutionEngine')
-rw-r--r--Source/ExecutionEngine/ExecutionEngine.cs3
1 files changed, 2 insertions, 1 deletions
diff --git a/Source/ExecutionEngine/ExecutionEngine.cs b/Source/ExecutionEngine/ExecutionEngine.cs
index eb871ac3..d1f09d2a 100644
--- a/Source/ExecutionEngine/ExecutionEngine.cs
+++ b/Source/ExecutionEngine/ExecutionEngine.cs
@@ -1041,8 +1041,9 @@ namespace Microsoft.Boogie
{
var s = StatisticsPerRequest[kv.Key];
var cacs = s.CachingActionCounts;
+ var c = cacs != null ? string.Format(", {0,3}, {1,3}, {2,3}, {3,3}, {4,3}, {5,3}", cacs[0], cacs[1], cacs[2], cacs[3], cacs[4], cacs[5]) : "";
var t = printTimes ? string.Format(", {0,8:F0}", kv.Value.TotalMilliseconds) : "";
- Console.Out.WriteLine("{0,-19}{1}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}, {7,3}, {8,3}, {9,3}, {10,3}, {11,3}, {12,3}", kv.Key, t, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount, cacs[0], cacs[1], cacs[2], cacs[3], cacs[4], cacs[5]);
+ Console.Out.WriteLine("{0,-19}{1}, {2,2}, {3,2}, {4,2}, {5,2}, {6,2}{7}", kv.Key, t, s.ErrorCount, s.InconclusiveCount, s.OutOfMemoryCount, s.TimeoutCount, s.VerifiedCount, c);
}
if (printTimes)