summaryrefslogtreecommitdiff
path: root/Source/Houdini
diff options
context:
space:
mode:
authorGravatar qadeer <qadeer@microsoft.com>2011-11-24 14:22:33 -0800
committerGravatar qadeer <qadeer@microsoft.com>2011-11-24 14:22:33 -0800
commit132b03c3c6032dd2db21eac27616f7212dbcbb52 (patch)
tree21c8197f2c15c92a1b9ab65d6b0b926221975dc2 /Source/Houdini
parentdf1cd695daffb01a590a7310dbee1b6594de2ecd (diff)
added some more statistics to houdini
added a coupe more regressions for houdini+inlineDepth
Diffstat (limited to 'Source/Houdini')
-rw-r--r--Source/Houdini/Checker.cs2
1 files changed, 2 insertions, 0 deletions
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index b0c8fabf..e36d32ef 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -19,6 +19,7 @@ using VC;
namespace Microsoft.Boogie.Houdini {
public class HoudiniSession {
public static double proverTime = 0;
+ public static int numProverQueries = 0;
private string descriptiveName;
private VCExpr conjecture;
private ProverInterface.ErrorHandler handler;
@@ -56,6 +57,7 @@ namespace Microsoft.Boogie.Houdini {
WaitHandle.WaitAny(new WaitHandle[] { checker.ProverDone });
ProverInterface.Outcome proverOutcome = checker.ReadOutcome();
proverTime += (DateTime.Now - now).TotalSeconds;
+ numProverQueries++;
if (proverOutcome == ProverInterface.Outcome.Invalid) {
Contract.Assume(collector.examples != null);