Extra debugging output for Houdini

1 files changed, 18 insertions, 0 deletions

diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 526302db..b47512bd 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -568,6 +568,8 @@ namespace Microsoft.Boogie.Houdini {
     private void UpdateAssignment(RefutedAnnotation refAnnot) {

       if (CommandLineOptions.Clo.Trace) {

         Console.WriteLine("Removing " + refAnnot.Constant);

+        using (var cexWriter = new System.IO.StreamWriter("houdiniCexTrace.bpl", true))

+            cexWriter.WriteLine("Removing " + refAnnot.Constant);

       }

       currentHoudiniState.Assignment.Remove(refAnnot.Constant);

       currentHoudiniState.Assignment.Add(refAnnot.Constant, false);

@@ -603,6 +605,22 @@ namespace Microsoft.Boogie.Houdini {
               AddRelatedToWorkList(refutedAnnotation);

               UpdateAssignment(refutedAnnotation);

               dequeue = false;

+              #region Extra debugging output

+              if (CommandLineOptions.Clo.Trace)

+              {

+                  using (var cexWriter = new System.IO.StreamWriter("houdiniCexTrace.bpl", true))

+                  {

+                      cexWriter.WriteLine("Counter example for " + refutedAnnotation.Constant);

+                      cexWriter.Write(error.ToString());

+                      cexWriter.WriteLine();

+                      using (var writer = new Microsoft.Boogie.TokenTextWriter(cexWriter))

+                          foreach (Microsoft.Boogie.Block blk in error.Trace)

+                              blk.Emit(writer, 15);

+                      //cexWriter.WriteLine(); 

+                  }

+              }

+              #endregion

+

             }

           }

           break;