remove a redundant member function that I added before

diff --git a/execution.cc b/execution.cc
index 9ee915708edd18550266126af75ad746c8f3544e..524c6fa2f2dded24e3421f533c88bb55a621fb6e 100644 (file)
--- a/execution.cc
+++ b/execution.cc
@@ -199,16 +199,6 @@ bool ModelExecution::have_bug_reports() const
        return priv->bugs.size() != 0;
 }
 
-/** @return True, if any fatal bugs have been reported for this execution.
- *  Any bug other than a data race is considered a fatal bug. Data races
- *  are not considered fatal unless the number of races is exceeds
- *  a threshold (temporarily set as 15).
- */
-bool ModelExecution::have_fatal_bug_reports() const
-{
-       return priv->bugs.size() != 0;
-}
-
 SnapVector<bug_message *> * ModelExecution::get_bugs() const
 {
        return &priv->bugs;

diff --git a/execution.h b/execution.h
index a6add070aa288d93555ae2382315019c09b04f13..24738828da635fb45cad052836a7669fba6eb089 100644 (file)
--- a/execution.h
+++ b/execution.h
@@ -70,7 +70,6 @@ public:
        bool assert_bug(const char *msg);
 
        bool have_bug_reports() const;
-       bool have_fatal_bug_reports() const;
 
        SnapVector<bug_message *> * get_bugs() const;
 

diff --git a/model.cc b/model.cc
index 0a2e844d32e2136e582600f1858574c143f5bd53..ce598cfa58302841e5cfe4ea0c2c5e8c3f036a1c 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -363,7 +363,7 @@ bool ModelChecker::should_terminate_execution()
        /* Infeasible -> don't take any more steps */
        if (execution->is_infeasible())
                return true;
-       else if (execution->isfeasibleprefix() && execution->have_fatal_bug_reports()) {
+       else if (execution->isfeasibleprefix() && execution->have_bug_reports()) {
                execution->set_assert();
                return true;
        } else if (execution->isFinished()) {