X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=cbd5617d8238f9326720fbcfb7dfb9c08864b6e3;hb=c0c175fd2688c46595d5aadf029026e147ec80c2;hp=feda416222de94f460291ee7f6a6ea15a21ddf22;hpb=1ad7373e04c1b94a927f4b8735bffe2c62af55f3;p=model-checker.git

diff --git a/model.cc b/model.cc
index feda416..cbd5617 100644
--- a/model.cc
+++ b/model.cc
@@ -2,6 +2,7 @@
 #include <algorithm>
 #include <mutex>
 #include <new>
+#include <stdarg.h>
 
 #include "model.h"
 #include "action.h"
@@ -419,9 +420,16 @@ bool ModelChecker::is_complete_execution() const
  * @param msg Descriptive message for the bug (do not include newline char)
  * @return True if bug is immediately-feasible
  */
-bool ModelChecker::assert_bug(const char *msg)
+bool ModelChecker::assert_bug(const char *msg, ...)
 {
-	priv->bugs.push_back(new bug_message(msg));
+	char str[800];
+
+	va_list ap;
+	va_start(ap, msg);
+	vsnprintf(str, sizeof(str), msg, ap);
+	va_end(ap);
+
+	priv->bugs.push_back(new bug_message(str));
 
 	if (isfeasibleprefix()) {
 		set_assert();