diff --git a/examples/tptp/tptp5.tab.c b/examples/tptp/tptp5.tab.c
index 7fcf7915b..c97225f4c 100644
--- a/examples/tptp/tptp5.tab.c
+++ b/examples/tptp/tptp5.tab.c
@@ -107,7 +107,7 @@ struct pTreeNode {
     pTree children[MAX_CHILDREN+1];
 };
 //-----------------------------------------------------------------------------
-int yyerror( char *s ) { 
+int yyerror( char const *s ) { 
 
     fprintf( stderr, "%s in line %d at item \"%s\".\n", s, yylineno, yytext); 
 	return 0;
diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp
index c23f222e5..218f9906a 100644
--- a/src/muz/base/dl_util.cpp
+++ b/src/muz/base/dl_util.cpp
@@ -34,8 +34,6 @@ Revision History:
 
 namespace datalog {
 
-    static unsigned verbose_action_inside = 0;
-
     verbose_action::verbose_action(char const* msg, unsigned lvl): m_lvl(lvl), m_sw(0) {
         IF_VERBOSE(m_lvl, 
                    (verbose_stream() << msg << "...").flush(); 
diff --git a/src/muz/rel/dl_lazy_table.cpp b/src/muz/rel/dl_lazy_table.cpp
index 16dbc2d21..ec97a4bf5 100644
--- a/src/muz/rel/dl_lazy_table.cpp
+++ b/src/muz/rel/dl_lazy_table.cpp
@@ -19,7 +19,7 @@ Revision History:
 
 #include "dl_lazy_table.h"
 #include "dl_relation_manager.h"
-#include <strstream>
+#include <sstream>
 
 namespace datalog {
 
@@ -53,7 +53,6 @@ namespace datalog {
         virtual table_base* operator()(const table_base& _t1, const table_base& _t2) {
             lazy_table const& t1 = get(_t1);
             lazy_table const& t2 = get(_t2);
-            lazy_table_plugin& p = t1.get_lplugin();
             lazy_table_ref* tr = alloc(lazy_table_join, m_cols1.size(), m_cols1.c_ptr(), m_cols2.c_ptr(), t1, t2, get_result_signature());
             return alloc(lazy_table, tr);
         }
diff --git a/src/muz/rel/dl_lazy_table.h b/src/muz/rel/dl_lazy_table.h
index 34a8b6b92..3c0b47367 100644
--- a/src/muz/rel/dl_lazy_table.h
+++ b/src/muz/rel/dl_lazy_table.h
@@ -156,7 +156,7 @@ namespace datalog {
         virtual table_base::iterator begin() const;
         virtual table_base::iterator end() const;
 
-        lazy_table_ref* ref() const { return m_ref.get(); }
+        lazy_table_ref* get_ref() const { return m_ref.get(); }
         void set(lazy_table_ref* r) { m_ref = r; }
     };
 
@@ -184,8 +184,8 @@ namespace datalog {
             : lazy_table_ref(t1.get_lplugin(), sig), 
               m_cols1(col_cnt, cols1), 
               m_cols2(col_cnt, cols2),
-              m_t1(t1.ref()),
-              m_t2(t2.ref()) { }
+              m_t1(t1.get_ref()),
+              m_t2(t2.get_ref()) { }
         virtual ~lazy_table_join() {}
         virtual lazy_table_kind kind() const { return LAZY_TABLE_JOIN; }
         unsigned_vector const& cols1() const { return m_cols1; }
@@ -203,7 +203,7 @@ namespace datalog {
         lazy_table_project(unsigned col_cnt, const unsigned * cols, lazy_table const& src, table_signature const& sig)
             : lazy_table_ref(src.get_lplugin(), sig), 
               m_cols(col_cnt, cols), 
-              m_src(src.ref()) {}
+              m_src(src.get_ref()) {}
         virtual ~lazy_table_project() {}
         
         virtual lazy_table_kind kind() const { return LAZY_TABLE_PROJECT; }
@@ -219,7 +219,7 @@ namespace datalog {
         lazy_table_rename(unsigned col_cnt, const unsigned * cols, lazy_table const& src, table_signature const& sig)
             : lazy_table_ref(src.get_lplugin(), sig), 
               m_cols(col_cnt, cols), 
-              m_src(src.ref()) {}
+              m_src(src.get_ref()) {}
         virtual ~lazy_table_rename() {}
         
         virtual lazy_table_kind kind() const { return LAZY_TABLE_RENAME; }
@@ -233,7 +233,7 @@ namespace datalog {
         ref<lazy_table_ref>      m_src;
     public:
         lazy_table_filter_identical(unsigned col_cnt, const unsigned * cols, lazy_table const& src)
-            : lazy_table_ref(src.get_lplugin(), src.get_signature()), m_cols(col_cnt, cols), m_src(src.ref()) {}
+            : lazy_table_ref(src.get_lplugin(), src.get_signature()), m_cols(col_cnt, cols), m_src(src.get_ref()) {}
         virtual ~lazy_table_filter_identical() {}
         
         virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_IDENTICAL; }
@@ -251,7 +251,7 @@ namespace datalog {
             : lazy_table_ref(src.get_lplugin(), src.get_signature()), 
             m_col(col), 
             m_value(value), 
-            m_src(src.ref()) {}
+            m_src(src.get_ref()) {}
         virtual ~lazy_table_filter_equal() {}
         
         virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_EQUAL; }
@@ -267,7 +267,7 @@ namespace datalog {
     public:
         lazy_table_filter_interpreted(lazy_table const& src, app* condition)
             : lazy_table_ref(src.get_lplugin(), src.get_signature()), 
-              m_condition(condition, src.get_lplugin().get_ast_manager()), m_src(src.ref()) {}
+              m_condition(condition, src.get_lplugin().get_ast_manager()), m_src(src.get_ref()) {}
         virtual ~lazy_table_filter_interpreted() {}
         
         virtual lazy_table_kind kind() const { return LAZY_TABLE_FILTER_INTERPRETED; }
@@ -286,8 +286,8 @@ namespace datalog {
         lazy_table_filter_by_negation(lazy_table const& tgt, lazy_table const& src, 
                                       unsigned_vector const& c1, unsigned_vector const& c2) 
         : lazy_table_ref(tgt.get_lplugin(), tgt.get_signature()),
-            m_tgt(tgt.ref()), 
-            m_src(src.ref()), 
+            m_tgt(tgt.get_ref()), 
+            m_src(src.get_ref()), 
             m_cols1(c1),
             m_cols2(c2) {}
         virtual ~lazy_table_filter_by_negation() {}