Merge pull request #108 from michael-emmi/restore-totalusertime

Restoring TotalUserTime increment removed by #106.
boogie-org · Jan 2, 2020 · 7d0b814 · 7d0b814
2 parents 316de1b + 071cf3b
commit 7d0b814
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 9 deletions.
diff --git a/boogie b/boogie
diff --git 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")));
+4 −3		Source/Concurrency/CivlTypeChecker.cs
+8 −15		Source/Concurrency/RefinementInstrumentation.cs
+1 −22		Source/Concurrency/YieldingProcChecker.cs
+24 −8		Source/Concurrency/YieldingProcDuplicator.cs
+52 −0		Source/Core/AbsyCmd.cs
+13 −1		Source/Provers/SMTLib/SMTLibProcess.cs
+6 −3		Test/civl/GC.bpl
+1 −8		Test/civl/linear-set.bpl
+1 −1		Test/civl/linear-set.bpl.expect
+3 −3		Test/civl/linear/typecheck.bpl
+1 −9		Test/civl/parallel2.bpl
+1 −1		Test/civl/parallel2.bpl.expect
+1 −9		Test/civl/parallel4.bpl
+4 −4		Test/civl/parallel4.bpl.expect
+1 −8		Test/civl/parallel5.bpl
+1 −1		Test/civl/parallel5.bpl.expect
+1 −1		Test/civl/podelski/x_perm.bpl
+1 −1		Test/civl/podelski/x_perm.bpl.expect