diff options
author | 2012-02-06 13:55:42 -0800 | |
---|---|---|
committer | 2012-02-06 13:55:42 -0800 | |
commit | 6a1cfac0a8625cb91ab61fc20f06d40c098654c2 (patch) | |
tree | 6130df9a4df19a35baf72efbd0a426dab3897a52 | |
parent | 2cfd14bafce9306ec3b62cdd119ccbba5caccac3 (diff) |
added more logging in houdini
-rw-r--r-- | Source/Houdini/Checker.cs | 2 | ||||
-rw-r--r-- | Source/Houdini/Houdini.cs | 6 |
2 files changed, 7 insertions, 1 deletions
diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs index 08d8346a..40d54a49 100644 --- a/Source/Houdini/Checker.cs +++ b/Source/Houdini/Checker.cs @@ -20,7 +20,7 @@ namespace Microsoft.Boogie.Houdini { public class HoudiniSession {
public static double proverTime = 0;
public static int numProverQueries = 0;
- private string descriptiveName;
+ public string descriptiveName;
private VCExpr conjecture;
private ProverInterface.ErrorHandler handler;
ConditionGeneration.CounterexampleCollector collector;
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs index 1f3909e4..7c043906 100644 --- a/Source/Houdini/Houdini.cs +++ b/Source/Houdini/Houdini.cs @@ -1190,6 +1190,12 @@ namespace Microsoft.Boogie.Houdini { this.NotifyAssignment(current.Assignment);
//check the VC with the current assignment
+ if (CommandLineOptions.Clo.Trace) {
+ Console.WriteLine("Verifying " + session.descriptiveName + " with the following assignment:");
+ foreach (var key in current.Assignment.Keys) {
+ Console.WriteLine(key + " -> " + current.Assignment[key]);
+ }
+ }
outcome = session.Verify(checker, currentAx, out errors);
this.NotifyOutcome(outcome);
|