model: add promise printing to execution summaries

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index c713d1e1761b308cc5433dfa05345a8c23d5024a..62550da7f4bd30398650b188ddc13dc1b82d1986 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2872,6 +2872,14 @@ void ModelChecker::print_summary() const
                print_infeasibility(" INFEASIBLE");
        print_list(action_trace);
        model_print("\n");
+       if (!promises->empty()) {
+               model_print("Pending promises:\n");
+               for (unsigned int i = 0; i < promises->size(); i++) {
+                       model_print(" [P%u] ", i);
+                       (*promises)[i]->print();
+               }
+               model_print("\n");
+       }
 }
 
 /**