From 400f15b0215dff25d4c1a252fcdb4e148975367f Mon Sep 17 00:00:00 2001
From: Jerry James <loganjerry@gmail.com>
Date: May 14 2015 03:14:51 +0000
Subject: New upstream release.  Drop upstreamed -messaget patch.


---

diff --git a/.gitignore b/.gitignore
index e0d72e0..32ee5af 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
 /cbmc-5.0.tar.xz
+/cbmc-5.1.tar.xz
diff --git a/cbmc-5.0-fix-build.patch b/cbmc-5.0-fix-build.patch
deleted file mode 100644
index afbf92d..0000000
--- a/cbmc-5.0-fix-build.patch
+++ /dev/null
@@ -1,96 +0,0 @@
-Index: src/cbmc/Makefile
-===================================================================
---- src/cbmc/Makefile	(revision 5150)
-+++ src/cbmc/Makefile	(working copy)
-@@ -23,7 +23,7 @@
- 
- INCLUDES= -I ..
- 
--LIBS =
-+LIBS = -lminisat -lcuddobj -lcudd -lmtr -lcuddst -lcuddutil -lepd -ldddmp
- 
- include ../config.inc
- include ../common
-Index: src/common
-===================================================================
---- src/common	(revision 5150)
-+++ src/common	(working copy)
-@@ -69,7 +69,7 @@
-   endif
- else
-   LINKLIB = ar rcT $@ $^
--  LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
-+  LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LDFLAGS) $(LIBS)
-   LINKNATIVE = $(HOSTCXX) -o $@ $^
-   ifeq ($(origin CC),default)
-     CC     = gcc
-Index: src/config.inc
-===================================================================
---- src/config.inc	(revision 5150)
-+++ src/config.inc	(working copy)
-@@ -4,18 +4,22 @@
- # Variables you may want to override
- #CXXFLAGS = -Wall -O0 -g -Werror -Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing -pedantic
- #CXXFLAGS = -std=c++11
-+CFLAGS = @RPM_OPT_FLAGS@
-+CXXFLAGS = @RPM_OPT_FLAGS@
-+LDFLAGS = @RPM_LD_FLAGS@
- 
- # If GLPK is available; this is used by goto-instrument and musketeer.
--#LIB_GLPK = -lglpk 
-+LIB_GLPK = -lglpk 
- 
- # SAT-solvers we have
- #PRECOSAT = ../../precosat-576-7e5e66f-120112
- #PICOSAT = ../../picosat-959
-+CUDD = /usr
- #LINGELING = ../../lingeling-587f-4882048-110513
- #CHAFF = ../../zChaff
- #BOOLEFORCE = ../../booleforce-0.4
- #MINISAT = ../../MiniSat-p_v1.14
--MINISAT2 = ../../minisat-2.2.0
-+MINISAT2 = /usr/include/minisat
- #GLUCOSE = ../../glucose2.2
- #SMVSAT =
- 
-Index: src/goto-instrument/Makefile
-===================================================================
---- src/goto-instrument/Makefile	(revision 5150)
-+++ src/goto-instrument/Makefile	(working copy)
-@@ -39,7 +39,7 @@
- 
- INCLUDES= -I ..
- 
--LIBS = 
-+LIBS = -lminisat -lcuddobj -lcudd -lmtr -lcuddst -lcuddutil -lepd -ldddmp
- 
- CLEANFILES = goto-instrument$(EXEEXT)
- 
-Index: src/solvers/Makefile
-===================================================================
---- src/solvers/Makefile	(revision 5150)
-+++ src/solvers/Makefile	(working copy)
-@@ -17,7 +17,7 @@
- ifneq ($(MINISAT2),)
-   MINISAT2_SRC=sat/satcheck_minisat2.cpp
-   MINISAT2_INCLUDE=-I $(MINISAT2)
--  MINISAT2_LIB=$(MINISAT2)/simp/SimpSolver$(OBJEXT) $(MINISAT2)/core/Solver$(OBJEXT)
-+#  MINISAT2_LIB=$(MINISAT2)/simp/SimpSolver$(OBJEXT) $(MINISAT2)/core/Solver$(OBJEXT)
-   CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
-   override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
- endif
-@@ -44,10 +44,10 @@
- 
- ifneq ($(CUDD),)
-   CUDD_SRC=qbf/qbf_bdd_core.cpp qbf/qbf_skizzo_core.cpp
--  CUDD_INCLUDE=-I $(CUDD)/include
--  CUDD_LIB=-L $(CUDD)/cudd -L $(CUDD)/util -L $(CUDD)/mtr \
--           -L $(CUDD)/st -L $(CUDD)/obj -L $(CUDD)/dddmp \
--           -L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
-+  CUDD_INCLUDE=-I $(CUDD)/include/cudd
-+#  CUDD_LIB=-L $(CUDD)/cudd -L $(CUDD)/util -L $(CUDD)/mtr \
-+#           -L $(CUDD)/st -L $(CUDD)/obj -L $(CUDD)/dddmp \
-+#           -L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
- endif
- 
- ifneq ($(PRECOSAT),)
diff --git a/cbmc-5.0-messaget.patch b/cbmc-5.0-messaget.patch
deleted file mode 100644
index 3c71f49..0000000
--- a/cbmc-5.0-messaget.patch
+++ /dev/null
@@ -1,349 +0,0 @@
-Index: src/solvers/qbf/qbf_bdd_core.cpp
-===================================================================
---- src/solvers/qbf/qbf_bdd_core.cpp	(revision 5150)
-+++ src/solvers/qbf/qbf_bdd_core.cpp	(working copy)
-@@ -194,7 +194,7 @@
-       solver_text() + ": "+
-       i2string(no_variables())+" variables, "+
-       i2string(matrix->nodeCount())+" nodes";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
- 
-   model_bdds.resize(no_variables()+1, NULL);
-@@ -419,7 +419,7 @@
- 
- void qbf_bdd_coret::compress_certificate(void)
- {
--  status("Compressing Certificate");
-+  status() << "Compressing Certificate" << eom;
- 
-   for(quantifierst::const_iterator it=quantifiers.begin();
-       it!=quantifiers.end();
-Index: src/solvers/qbf/qbf_skizzo_core.cpp
-===================================================================
---- src/solvers/qbf/qbf_skizzo_core.cpp	(revision 5150)
-+++ src/solvers/qbf/qbf_skizzo_core.cpp	(working copy)
-@@ -104,7 +104,7 @@
-       "Skizzo: "+
-       i2string(no_variables())+" variables, "+
-       i2string(no_clauses())+" clauses";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
- 
-   std::string result_tmp_file="sKizzo.out";
-@@ -156,7 +156,7 @@
- 
-     if(!result_found)
-     {
--      messaget::error("Skizzo failed: unknown result");
-+      messaget::error() << "Skizzo failed: unknown result" << messaget::eom;
-       return P_ERROR;
-     }
-   }
-@@ -166,7 +166,7 @@
- 
-   if(result)
-   {
--    messaget::status("Skizzo: TRUE");
-+    messaget::status() << "Skizzo: TRUE" << messaget::eom;
- 
-     if(get_certificate())
-       return P_ERROR;
-@@ -175,7 +175,7 @@
-   }
-   else
-   {
--    messaget::status("Skizzo: FALSE");
-+    messaget::status() << "Skizzo: FALSE" << messaget::eom;
-     return P_UNSATISFIABLE;
-   }
- }
-@@ -260,7 +260,7 @@
- 
-   if(!result)
-   {
--    messaget::error("Skizzo failed: unknown result");
-+    messaget::error() << "Skizzo failed: unknown result" << messaget::eom;
-     return true;
-   }
- 
-Index: src/solvers/qbf/qbf_squolem.cpp
-===================================================================
---- src/solvers/qbf/qbf_squolem.cpp	(revision 5150)
-+++ src/solvers/qbf/qbf_squolem.cpp	(working copy)
-@@ -96,7 +96,7 @@
-       "Squolem: "+
-       i2string(no_variables())+" variables, "+
-       i2string(no_clauses())+" clauses";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
- 
-   if(early_decision) return P_UNSATISFIABLE;
-@@ -113,12 +113,12 @@
- 
-   if(result)
-   {
--    messaget::status("Squolem: VALID");
-+    messaget::status() << "Squolem: VALID" << messaget::eom;
-     return P_SATISFIABLE;
-   }
-   else
-   {
--    messaget::status("Squolem: INVALID");
-+    messaget::status() << "Squolem: INVALID" << messaget::eom;
-     return P_UNSATISFIABLE;
-   }
- 
-Index: src/solvers/qbf/qbf_squolem_core.cpp
-===================================================================
---- src/solvers/qbf/qbf_squolem_core.cpp	(revision 5150)
-+++ src/solvers/qbf/qbf_squolem_core.cpp	(working copy)
-@@ -168,7 +168,7 @@
-       "Squolem: "+
-       i2string(no_variables())+" variables, "+
-       i2string(no_clauses())+" clauses";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
- 
-   squolem->endOfOriginals();
-@@ -176,12 +176,12 @@
- 
-   if(result)
-   {
--    messaget::status("Squolem: VALID");
-+    messaget::status() << "Squolem: VALID" << messaget::eom;
-     return P_SATISFIABLE;
-   }
-   else
-   {
--    messaget::status("Squolem: INVALID");
-+    messaget::status() << "Squolem: INVALID" << messaget::eom;
-     return P_UNSATISFIABLE;
-   }
- 
-Index: src/solvers/sat/satcheck_booleforce.cpp
-===================================================================
---- src/solvers/sat/satcheck_booleforce.cpp	(revision 5150)
-+++ src/solvers/sat/satcheck_booleforce.cpp	(working copy)
-@@ -188,7 +188,7 @@
-       break;    
-     }
- 
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
- 
-   if(result==BOOLEFORCE_UNSATISFIABLE)
-Index: src/solvers/sat/satcheck_glucose.cpp
-===================================================================
---- src/solvers/sat/satcheck_glucose.cpp	(revision 5150)
-+++ src/solvers/sat/satcheck_glucose.cpp	(working copy)
-@@ -203,7 +203,7 @@
-     std::string msg=
-       i2string(_no_variables)+" variables, "+
-       i2string(solver->nClauses())+" clauses";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
-   
-   add_variables();
-@@ -213,12 +213,12 @@
-   if(empty_clause_added)
-   {
-     msg="empty clause: negated claim is UNSATISFIABLE, i.e., holds";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom
-   }
-   else if(!solver->okay())
-   {
-     msg="SAT checker inconsistent: negated claim is UNSATISFIABLE, i.e., holds";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
-   else
-   {
-@@ -228,7 +228,7 @@
-     if(solver->solve(solver_assumptions))
-     {
-       msg="SAT checker: negated claim is SATISFIABLE, i.e., does not hold";
--      messaget::status(msg);
-+      messaget::status() << msg << messaget::eom;
-       assert(solver->model.size()!=0);
-       status=SAT;
-       return P_SATISFIABLE;
-@@ -236,7 +236,7 @@
-     else
-     {
-       msg="SAT checker: negated claim is UNSATISFIABLE, i.e., holds";
--      messaget::status(msg);
-+      messaget::status() << msg << messaget::eom;
-     }
-   }
- 
-Index: src/solvers/sat/satcheck_limmat.cpp
-===================================================================
---- src/solvers/sat/satcheck_limmat.cpp	(revision 5150)
-+++ src/solvers/sat/satcheck_limmat.cpp	(working copy)
-@@ -158,7 +158,7 @@
-     std::string msg=
-       i2string(maxvar_Limmat(solver))+" variables, "+
-       i2string(clauses_Limmat(solver))+" clauses";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
- 
-   int status=sat_Limmat(solver, -1);
-@@ -181,7 +181,7 @@
-       break;    
-     }
- 
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
- 
-   if(status==0)
-Index: src/solvers/sat/satcheck_lingeling.cpp
-===================================================================
---- src/solvers/sat/satcheck_lingeling.cpp	(revision 5150)
-+++ src/solvers/sat/satcheck_lingeling.cpp	(working copy)
-@@ -118,7 +118,7 @@
-     std::string msg=
-       i2string(_no_variables)+" variables, "+
-       i2string(clause_counter)+" clauses";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
-   
-   std::string msg;
-@@ -130,7 +130,7 @@
-   if(res==10)
-   {
-     msg="SAT checker: negated claim is SATISFIABLE, i.e., does not hold";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-     status=SAT;
-     return P_SATISFIABLE;
-   }
-@@ -138,7 +138,7 @@
-   {
-     assert(res==20);
-     msg="SAT checker: negated claim is UNSATISFIABLE, i.e., holds";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
- 
-   status=UNSAT;
-Index: src/solvers/sat/satcheck_picosat.cpp
-===================================================================
---- src/solvers/sat/satcheck_picosat.cpp	(revision 5150)
-+++ src/solvers/sat/satcheck_picosat.cpp	(working copy)
-@@ -120,7 +120,7 @@
-     std::string msg=
-       i2string(_no_variables)+" variables, "+
-       i2string(picosat_added_original_clauses(picosat))+" clauses";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
-   
-   std::string msg;
-@@ -132,7 +132,7 @@
-   if(res==PICOSAT_SATISFIABLE)
-   {
-     msg="SAT checker: negated claim is SATISFIABLE, i.e., does not hold";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-     status=SAT;
-     return P_SATISFIABLE;
-   }
-@@ -140,7 +140,7 @@
-   {
-     assert(res==PICOSAT_UNSATISFIABLE);
-     msg="SAT checker: negated claim is UNSATISFIABLE, i.e., holds";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
- 
-   status=UNSAT;
-Index: src/solvers/sat/satcheck_precosat.cpp
-===================================================================
---- src/solvers/sat/satcheck_precosat.cpp	(revision 5150)
-+++ src/solvers/sat/satcheck_precosat.cpp	(working copy)
-@@ -118,7 +118,7 @@
-     std::string msg=
-       i2string(_no_variables)+" variables, "+
-       i2string(solver->getAddedOrigClauses())+" clauses";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
-   
-   std::string msg;
-@@ -127,7 +127,7 @@
-   if(res==1)
-   {
-     msg="SAT checker: negated claim is SATISFIABLE, i.e., does not hold";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-     status=SAT;
-     return P_SATISFIABLE;
-   }
-@@ -135,7 +135,7 @@
-   {
-     assert(res==-1);
-     msg="SAT checker: negated claim is UNSATISFIABLE, i.e., holds";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
- 
-   status=UNSAT;
-Index: src/solvers/sat/satcheck_smvsat.cpp
-===================================================================
---- src/solvers/sat/satcheck_smvsat.cpp	(revision 5150)
-+++ src/solvers/sat/satcheck_smvsat.cpp	(working copy)
-@@ -188,7 +188,7 @@
-       break;    
-     }
- 
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
- 
-   if(result==0)
-Index: src/solvers/sat/satcheck_zchaff.cpp
-===================================================================
---- src/solvers/sat/satcheck_zchaff.cpp	(revision 5150)
-+++ src/solvers/sat/satcheck_zchaff.cpp	(working copy)
-@@ -153,7 +153,7 @@
-     std::string msg=
-       i2string(solver->num_variables())+" variables, "+
-       i2string(solver->clauses().size())+" clauses";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
- 
-   SAT_StatusT result=(SAT_StatusT)solver->solve();
-@@ -192,7 +192,7 @@
-       break;    
-     }
- 
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
- 
-   if(result==SATISFIABLE)
-Index: src/solvers/sat/satcheck_zcore.cpp
-===================================================================
---- src/solvers/sat/satcheck_zcore.cpp	(revision 5150)
-+++ src/solvers/sat/satcheck_zcore.cpp	(working copy)
-@@ -101,7 +101,7 @@
-     std::string msg=
-       i2string(no_variables())+" variables, "+
-       i2string(no_clauses())+" clauses";
--    messaget::status(msg);
-+    messaget::status() << msg << messaget::eom;
-   }
- 
-   // get the core
diff --git a/cbmc-5.1-fix-build.patch b/cbmc-5.1-fix-build.patch
new file mode 100644
index 0000000..fd4d274
--- /dev/null
+++ b/cbmc-5.1-fix-build.patch
@@ -0,0 +1,96 @@
+Index: src/cbmc/Makefile
+===================================================================
+--- src/cbmc/Makefile	(revision 5391)
++++ src/cbmc/Makefile	(working copy)
+@@ -23,7 +23,7 @@
+ 
+ INCLUDES= -I ..
+ 
+-LIBS =
++LIBS = -lminisat -lcuddobj -lcudd -lmtr -lcuddst -lcuddutil -lepd -ldddmp
+ 
+ include ../config.inc
+ include ../common
+Index: src/common
+===================================================================
+--- src/common	(revision 5391)
++++ src/common	(working copy)
+@@ -69,7 +69,7 @@
+   endif
+ else
+   LINKLIB = ar rcT $@ $^
+-  LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LIBS)
++  LINKBIN = $(CXX) $(LINKFLAGS) -o $@ -Wl,--start-group $^ -Wl,--end-group $(LDFLAGS) $(LIBS)
+   LINKNATIVE = $(HOSTCXX) -o $@ $^
+   ifeq ($(origin CC),default)
+     CC     = gcc
+Index: src/config.inc
+===================================================================
+--- src/config.inc	(revision 5391)
++++ src/config.inc	(working copy)
+@@ -4,18 +4,22 @@
+ # Variables you may want to override
+ #CXXFLAGS = -Wall -O0 -g -Werror -Wno-long-long -Wno-sign-compare -Wno-parentheses -Wno-strict-aliasing -pedantic
+ #CXXFLAGS = -std=c++11
++CFLAGS = @RPM_OPT_FLAGS@
++CXXFLAGS = @RPM_OPT_FLAGS@
++LDFLAGS = @RPM_LD_FLAGS@
+ 
+ # If GLPK is available; this is used by goto-instrument and musketeer.
+-#LIB_GLPK = -lglpk 
++LIB_GLPK = -lglpk 
+ 
+ # SAT-solvers we have
+ #PRECOSAT = ../../precosat-576-7e5e66f-120112
+ #PICOSAT = ../../picosat-959
++CUDD = /usr
+ #LINGELING = ../../lingeling-587f-4882048-110513
+ #CHAFF = ../../zChaff
+ #BOOLEFORCE = ../../booleforce-0.4
+ #MINISAT = ../../MiniSat-p_v1.14
+-MINISAT2 = ../../minisat-2.2.0
++MINISAT2 = /usr/include/minisat
+ #GLUCOSE = ../../glucose2.2
+ #SMVSAT =
+ 
+Index: src/goto-instrument/Makefile
+===================================================================
+--- src/goto-instrument/Makefile	(revision 5391)
++++ src/goto-instrument/Makefile	(working copy)
+@@ -39,7 +39,7 @@
+ 
+ INCLUDES= -I ..
+ 
+-LIBS = 
++LIBS = -lminisat -lcuddobj -lcudd -lmtr -lcuddst -lcuddutil -lepd -ldddmp
+ 
+ CLEANFILES = goto-instrument$(EXEEXT)
+ 
+Index: src/solvers/Makefile
+===================================================================
+--- src/solvers/Makefile	(revision 5391)
++++ src/solvers/Makefile	(working copy)
+@@ -17,7 +17,7 @@
+ ifneq ($(MINISAT2),)
+   MINISAT2_SRC=sat/satcheck_minisat2.cpp
+   MINISAT2_INCLUDE=-I $(MINISAT2)
+-  MINISAT2_LIB=$(MINISAT2)/simp/SimpSolver$(OBJEXT) $(MINISAT2)/core/Solver$(OBJEXT)
++#  MINISAT2_LIB=$(MINISAT2)/simp/SimpSolver$(OBJEXT) $(MINISAT2)/core/Solver$(OBJEXT)
+   CP_CXXFLAGS += -DHAVE_MINISAT2 -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS
+   override CXXFLAGS := $(filter-out -pedantic, $(CXXFLAGS))
+ endif
+@@ -44,10 +44,10 @@
+ 
+ ifneq ($(CUDD),)
+   CUDD_SRC=qbf/qbf_bdd_core.cpp qbf/qbf_skizzo_core.cpp
+-  CUDD_INCLUDE=-I $(CUDD)/include
+-  CUDD_LIB=-L $(CUDD)/cudd -L $(CUDD)/util -L $(CUDD)/mtr \
+-           -L $(CUDD)/st -L $(CUDD)/obj -L $(CUDD)/dddmp \
+-           -L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
++  CUDD_INCLUDE=-I $(CUDD)/include/cudd
++#  CUDD_LIB=-L $(CUDD)/cudd -L $(CUDD)/util -L $(CUDD)/mtr \
++#           -L $(CUDD)/st -L $(CUDD)/obj -L $(CUDD)/dddmp \
++#           -L $(CUDD)/epd -lobj -lcudd -lmtr -lst -lutil -lepd -ldddmp
+ endif
+ 
+ ifneq ($(PRECOSAT),)
diff --git a/cbmc.spec b/cbmc.spec
index 0b81b88..4b21fb0 100644
--- a/cbmc.spec
+++ b/cbmc.spec
@@ -1,6 +1,6 @@
 Name:           cbmc
-Version:        5.0
-Release:        2%{?dist}
+Version:        5.1
+Release:        1%{?dist}
 Summary:        Bounded Model Checker for ANSI-C and C++ programs
 
 License:        BSD with advertising
@@ -14,9 +14,7 @@ Source0:        %{name}-%{version}.tar.xz
 # Man page link for goto-cc and goto-instrument
 Source1:        goto-cc.1
 # Fedora-specific patch: set up our build options
-Patch0:         %{name}-5.0-fix-build.patch
-# Finish applying an incomplete API change; sent upstream 2 Feb 2015
-Patch1:         %{name}-5.0-messaget.patch
+Patch0:         %{name}-5.1-fix-build.patch
 
 BuildRequires:  bison
 BuildRequires:  cudd-devel
@@ -36,7 +34,6 @@ iterations.
 %prep
 %setup -q
 %patch0
-%patch1
 
 # Use the right build flags
 sed -e "s|@RPM_OPT_FLAGS@|$RPM_OPT_FLAGS|" \
@@ -76,6 +73,10 @@ make -C regression
 %{_mandir}/man1/*
 
 %changelog
+* Wed May 13 2015 Jerry James <loganjerry@gmail.com> - 5.1-1
+- New upstream release
+- Drop upstreamed -messaget patch
+
 * Sat May 02 2015 Kalev Lember <kalevlember@gmail.com> - 5.0-2
 - Rebuilt for GCC 5 C++11 ABI change
 
diff --git a/sources b/sources
index 0110a9f..a14ca06 100644
--- a/sources
+++ b/sources
@@ -1 +1 @@
-5ca51f52407714e41bf3497e053bf798  cbmc-5.0.tar.xz
+3e148706b27f07850aac995b459b2330  cbmc-5.1.tar.xz