changes to support a configured errorLimit

3 files changed, 21 insertions, 8 deletions

diff --git a/Source/Houdini/Checker.cs b/Source/Houdini/Checker.cs
index 30d6062f..252321b6 100644
--- a/Source/Houdini/Checker.cs
+++ b/Source/Houdini/Checker.cs
@@ -130,13 +130,13 @@ namespace Microsoft.Boogie.Houdini {
       return false;

     }

 

-    public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats, int houdiniID = -1) {

+    public HoudiniSession(Houdini houdini, VCGen vcgen, ProverInterface proverInterface, Program program, Implementation impl, HoudiniStatistics stats, int taskID = -1) {

       this.descriptiveName = impl.Name;

       this.stats = stats;

       collector = new ConditionGeneration.CounterexampleCollector();

       collector.OnProgress("HdnVCGen", 0, 0, 0.0);

 

-      vcgen.ConvertCFG2DAG(impl, threadID: houdiniID);

+      vcgen.ConvertCFG2DAG(impl, taskID: taskID);

       ModelViewInfo mvInfo;

       var gotoCmdOrigins = vcgen.PassifyImpl(impl, out mvInfo);

 

@@ -222,7 +222,7 @@ namespace Microsoft.Boogie.Houdini {
       return expr;

     }

 

-    public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionary<Variable, bool> assignment, out List<Counterexample> errors) {

+    public ProverInterface.Outcome Verify(ProverInterface proverInterface, Dictionary<Variable, bool> assignment, out List<Counterexample> errors, int taskID = -1) {

       collector.examples.Clear();

 

       if (CommandLineOptions.Clo.Trace) {

@@ -232,7 +232,7 @@ namespace Microsoft.Boogie.Houdini {
 

       VCExpr vc = proverInterface.VCExprGen.Implies(BuildAxiom(proverInterface, assignment), conjecture);

       proverInterface.BeginCheck(descriptiveName, vc, handler);

-      ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler);

+      ProverInterface.Outcome proverOutcome = proverInterface.CheckOutcome(handler, taskID: taskID);

 

       double queryTime = (DateTime.UtcNow - now).TotalSeconds;

       stats.proverTime += queryTime;

diff --git a/Source/Houdini/ConcurrentHoudini.cs b/Source/Houdini/ConcurrentHoudini.cs
index a75cc054..f4bab257 100644
--- a/Source/Houdini/ConcurrentHoudini.cs
+++ b/Source/Houdini/ConcurrentHoudini.cs
@@ -43,7 +43,7 @@ namespace Microsoft.Boogie.Houdini
       Inline();
 
       this.vcgen = new VCGen(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List<Checker>());
-      this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime);
+      this.proverInterface = ProverInterface.CreateProver(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, CommandLineOptions.Clo.ProverKillTime, id);
 
       vcgenFailures = new HashSet<Implementation>();
       Dictionary<Implementation, HoudiniSession> houdiniSessions = new Dictionary<Implementation, HoudiniSession>();
@@ -53,7 +53,7 @@ namespace Microsoft.Boogie.Houdini
         try {
           if (CommandLineOptions.Clo.Trace)
             Console.WriteLine("Generating VC for {0}", impl.Name);
-          HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, id);
+          HoudiniSession session = new HoudiniSession(this, vcgen, proverInterface, program, impl, stats, taskID: id);
           houdiniSessions.Add(impl, session);
         }
         catch (VCGenException) {
@@ -260,5 +260,18 @@ namespace Microsoft.Boogie.Houdini
         }
       } 
     }
+
+    protected override ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {
+      ProverInterface.Outcome outcome;
+      try {
+        outcome = session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), out errors, taskID: id);
+      }
+      catch (UnexpectedProverOutputException upo) {
+        Contract.Assume(upo != null);
+        errors = null;
+        outcome = ProverInterface.Outcome.Undetermined;
+      }
+      return outcome;
+    }
   }
 }
diff --git a/Source/Houdini/Houdini.cs b/Source/Houdini/Houdini.cs
index 12c972f3..c3575800 100644
--- a/Source/Houdini/Houdini.cs
+++ b/Source/Houdini/Houdini.cs
@@ -1086,7 +1086,7 @@ namespace Microsoft.Boogie.Houdini {
       return null;

     }

 

-    protected ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {

+    protected virtual ProverInterface.Outcome TryCatchVerify(HoudiniSession session, int stage, IEnumerable<int> completedStages, out List<Counterexample> errors) {

       ProverInterface.Outcome outcome;

       try {

         outcome = session.Verify(proverInterface, GetAssignmentWithStages(stage, completedStages), out errors);

@@ -1099,7 +1099,7 @@ namespace Microsoft.Boogie.Houdini {
       return outcome;

     }

 

-    private Dictionary<Variable, bool> GetAssignmentWithStages(int currentStage, IEnumerable<int> completedStages)

+    protected Dictionary<Variable, bool> GetAssignmentWithStages(int currentStage, IEnumerable<int> completedStages)

     {

       Dictionary<Variable, bool> result = new Dictionary<Variable, bool>(currentHoudiniState.Assignment);

       foreach (var c in program.TopLevelDeclarations.OfType<Constant>())