Fixed bug breaking our consolidation of future values...

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index a22e0214a6c2a3fdabd01a5442b3cba6643c616d..0665ff49b9762c0e9317d5688d21437f614535ca 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -25,6 +25,7 @@ ModelChecker::ModelChecker(struct model_params params) :
        num_executions(0),
        num_feasible_executions(0),
        diverge(NULL),
+       earliest_diverge(NULL),
        action_trace(new action_list_t()),
        thread_map(new HashTable<int, Thread *, int>()),
        obj_map(new HashTable<const void *, action_list_t, uintptr_t, 4>()),
@@ -180,8 +181,13 @@ bool ModelChecker::next_execution()
        DBG();
 
        num_executions++;
-       if (isfinalfeasible())
+       if (isfinalfeasible()) {
+               printf("Earliest divergence point since last feasible execution:\n");
+               earliest_diverge->print();
+
+               earliest_diverge = NULL;
                num_feasible_executions++;
+       }
 
        if (isfinalfeasible() || DBG_ENABLED())
                print_summary();
@@ -189,6 +195,9 @@ bool ModelChecker::next_execution()
        if ((diverge = get_next_backtrack()) == NULL)
                return false;
 
+       if (earliest_diverge == NULL || *diverge < *earliest_diverge)
+               earliest_diverge=diverge;
+
        if (DBG_ENABLED()) {
                printf("Next execution will diverge at:\n");
                diverge->print();