From 071cf3be0410d30a63ad45fe6aa37c03a2dd8453 Mon Sep 17 00:00:00 2001 From: Michael Emmi Date: Thu, 2 Jan 2020 10:34:24 -0500 Subject: [PATCH] Restoring TotalUserTime increment removed by #106. --- boogie | 2 +- source/Driver.cs | 10 ++-------- 2 files changed, 3 insertions(+), 9 deletions(-) diff --git a/boogie b/boogie index 09ee32e20..c1c61afab 160000 --- a/boogie +++ b/boogie @@ -1 +1 @@ -Subproject commit 09ee32e20948aa455f60cdd74c07da3a8b7b9dbe +Subproject commit c1c61afab95a82b55a250701dba831fccab5e6c4 diff --git a/source/Driver.cs b/source/Driver.cs index fc388245d..b7a9af651 100644 --- a/source/Driver.cs +++ b/source/Driver.cs @@ -449,10 +449,7 @@ public static int run(string[] args) // Add our CPU time to Z3's CPU time reported by SMTLibProcess and print it Microsoft.Boogie.FixedpointVC.CleanUp(); // make sure to account for FixedPoint Time System.TimeSpan TotalUserTime = System.Diagnostics.Process.GetCurrentProcess().UserProcessorTime; - - // XXX: cannot count prover time this way because Boogie deleted this field. - // TotalUserTime += Microsoft.Boogie.SMTLib.SMTLibProcess.TotalUserTime; - + TotalUserTime += Microsoft.Boogie.SMTLib.SMTLibProcess.TotalUserTime; Log.WriteLine(string.Format("Total User CPU time: {0} s", TotalUserTime.TotalSeconds)); @@ -1215,10 +1212,7 @@ public static void runSDVMode(Program program, Configs config) // Add our CPU time to Z3's CPU time reported by SMTLibProcess and print it Microsoft.Boogie.FixedpointVC.CleanUp(); // make sure to account for FixedPoint Time System.TimeSpan TotalUserTime = System.Diagnostics.Process.GetCurrentProcess().UserProcessorTime; - - // XXX: cannot count prover time this way because Boogie deleted this field. - // TotalUserTime += Microsoft.Boogie.SMTLib.SMTLibProcess.TotalUserTime; - + TotalUserTime += Microsoft.Boogie.SMTLib.SMTLibProcess.TotalUserTime; Console.WriteLine(string.Format("Total User CPU time: {0} s", TotalUserTime.TotalSeconds.ToString("F2")));