diff options
| -rw-r--r-- | Source/Houdini/Houdini.cs | 18 |
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;
|