ExplainHoudini change to add reasons for inconsistency as well.

1 files changed, 8 insertions, 0 deletions

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 6ffaef22..30056d99 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -385,6 +385,9 @@ namespace Microsoft.Boogie.Houdini {
                 break;

 

             unsatisfiedSoftAssumptions2.Iter(i => reason.Remove(softAssumptions2[i].ToString()));

+            var reason1 = new HashSet<string>(); //these are the reasons for inconsistency

+            unsatisfiedSoftAssumptions2.Iter(i => reason1.Add(softAssumptions2[i].ToString()));

+

             if (CommandLineOptions.Clo.Trace)

             {

                 Console.Write("Revised reason for removal of {0}: ", refutedConstant.Name);

@@ -395,6 +398,11 @@ namespace Microsoft.Boogie.Houdini {
             {

                 Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=red ];", refutedConstant.Name, r, descriptiveName);

             }

+            //also add the removed reasons using dotted edges (requires- x != 0, requires- x == 0 ==> assert x != 0)

+            foreach (var r in reason1)

+            {

+                Houdini.explainHoudiniDottyFile.WriteLine("{0} -> {1} [ label = \"{2}\" color=blue style=dotted ];", refutedConstant.Name, r, descriptiveName);

+            }

         } while (false);

 

         if (outcome == ProverInterface.Outcome.TimeOut || outcome == ProverInterface.Outcome.OutOfMemory || outcome == ProverInterface.Outcome.Undetermined)