From 5ce95a517568b618b54e2bc401a9314d2a202ef5 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Tue, 30 May 2017 11:34:38 +0200
Subject: [PATCH 1/2] Adapt print/messaget API, get_error_found

---
 src/vcegar/abstractor.cpp              | 10 ++++++----
 src/vcegar/modelchecker_smv.cpp        |  2 +-
 src/verilog/verilog_typecheck_expr.cpp |  7 +++++--
 3 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/src/vcegar/abstractor.cpp b/src/vcegar/abstractor.cpp
index 2102978c2..8a5597c8e 100644
--- a/src/vcegar/abstractor.cpp
+++ b/src/vcegar/abstractor.cpp
@@ -572,8 +572,9 @@ void abstractort::calc_abstract_trans_rel(
     throw "unexpected result from predabs_sat1.solve()";
   }
 
-  print(9, "Generated "+
-    i2string(trans_cube_set.no_insertions())+" cube(s)");
+  debug() <<"Generated "
+          << i2string(trans_cube_set.no_insertions()) << " cube(s)"
+          << eom;
 
   if(show_cubes)
     std::cout << trans_cube_set;
@@ -693,8 +694,9 @@ void abstractort::calc_abstract_initial_states(
   }
 
   // std::cout<<" The abstract transition relation \n";
-  print(9, "Generated "+
-    i2string(initial.no_insertions())+" cube(s)\n");
+  debug() << "Generated " <<
+          << i2string(initial.no_insertions()) <, " cube(s)\n"
+          << eom;
 
   if(show_cubes)
     std::cout << initial;
diff --git a/src/vcegar/modelchecker_smv.cpp b/src/vcegar/modelchecker_smv.cpp
index d5ccf95d1..922346208 100644
--- a/src/vcegar/modelchecker_smv.cpp
+++ b/src/vcegar/modelchecker_smv.cpp
@@ -164,7 +164,7 @@ bool modelchecker_smvt::read_result_cadence_smv(
           counterexample);
 
 
-        print(9, "Cadence SMV counterexample sucessfully read");
+        debug() << "Cadence SMV counterexample sucessfully read" << eom;
 
         return false;
       }
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index 03a98c7aa..0228639a1 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -2026,6 +2026,9 @@ bool verilog_typecheck(
   message_handlert &message_handler,
   const namespacet &ns)
 {
+  const unsigned errors_before=
+    message_handler.get_message_count(messaget::M_ERROR);
+
   verilog_typecheck_exprt verilog_typecheck_expr(
     ns, module_identifier, message_handler);
 
@@ -2048,6 +2051,6 @@ bool verilog_typecheck(
   {
     verilog_typecheck_expr.error() << e << messaget::eom;
   }
-  
-  return verilog_typecheck_expr.get_error_found();
+
+  return message_handler.get_message_count(messaget::M_ERROR)!=errors_before;
 }

From 7328b2ea64e44f2760b2443037c625aa4409793f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= <matthias.guedemann@diffblue.com>
Date: Wed, 7 Jun 2017 08:34:45 +0200
Subject: [PATCH 2/2] Adapt Makefile of EBMC to new location of c_types

---
 src/ebmc/Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ebmc/Makefile b/src/ebmc/Makefile
index efe425b8b..719aa85b7 100644
--- a/src/ebmc/Makefile
+++ b/src/ebmc/Makefile
@@ -9,7 +9,7 @@ SRC = diameter.cpp main.cpp diatest.cpp show_properties.cpp \
 OBJ+= $(CBMC)/src/util/util$(LIBEXT) \
       $(CBMC)/src/langapi/langapi$(LIBEXT) \
       $(CBMC)/src/ansi-c/string_constant$(OBJEXT) \
-      $(CBMC)/src/ansi-c/c_types$(OBJEXT) \
+      $(CBMC)/src/util/c_types$(OBJEXT) \
       $(CBMC)/src/solvers/solvers$(LIBEXT) \
       $(CBMC)/src/big-int/big-int$(LIBEXT) \
       ../trans-netlist/trans-netlist$(LIBEXT) \