X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=97e112f4b16ce149109a41bc9349c32930ce998f;hb=dc0339b4449ed07afa7c69936108146d72676a68;hp=33e8805078b546ac8d1b4f87dab3ea31e9be2651;hpb=ecf16617a0c289981925fcd2437595f3a2fce8fe;p=model-checker.git

diff --git a/model.cc b/model.cc
index 33e8805..97e112f 100644
--- a/model.cc
+++ b/model.cc
@@ -337,45 +337,30 @@ bool ModelChecker::is_complete_execution() const
  * the current trace is not yet feasible, the error message will be stashed and
  * printed if the execution ever becomes feasible.
  *
- * This function can also be used to immediately trigger the bug; that is, we
- * don't wait for a feasible execution before aborting. Only use the
- * "immediate" option when you know that the infeasibility is justified (e.g.,
- * pending release sequences are not a problem)
- *
  * @param msg Descriptive message for the bug (do not include newline char)
- * @param user_thread Was this assertion triggered from a user thread?
- * @param immediate Should this bug be triggered immediately?
+ * @return True if bug is immediately-feasible
  */
-void ModelChecker::assert_bug(const char *msg, bool user_thread, bool immediate)
+bool ModelChecker::assert_bug(const char *msg)
 {
 	priv->bugs.push_back(new bug_message(msg));
 
-	if (immediate || isfeasibleprefix()) {
+	if (isfeasibleprefix()) {
 		set_assert();
-		if (user_thread)
-			switch_to_master(NULL);
+		return true;
 	}
+	return false;
 }
 
 /**
- * @brief Assert a bug in the executing program, with a default message
- * @see ModelChecker::assert_bug
- * @param user_thread Was this assertion triggered from a user thread?
- */
-void ModelChecker::assert_bug(bool user_thread)
-{
-	assert_bug("bug detected", user_thread);
-}
-
-/**
- * @brief Assert a bug in the executing program immediately
+ * @brief Assert a bug in the executing program, asserted by a user thread
  * @see ModelChecker::assert_bug
  * @param msg Descriptive message for the bug (do not include newline char)
  */
-void ModelChecker::assert_bug_immediate(const char *msg)
+void ModelChecker::assert_user_bug(const char *msg)
 {
-	printf("Feasible: %s\n", isfeasibleprefix() ? "yes" : "no");
-	assert_bug(msg, false, true);
+	/* If feasible bug, bail out now */
+	if (assert_bug(msg))
+		switch_to_master(NULL);
 }
 
 /** @return True, if any bugs have been reported for this execution */