diff --git a/src/muz_qe/dl_boogie_proof.cpp b/src/muz_qe/dl_boogie_proof.cpp
index 8720b3544..e14512973 100644
--- a/src/muz_qe/dl_boogie_proof.cpp
+++ b/src/muz_qe/dl_boogie_proof.cpp
@@ -176,7 +176,7 @@ namespace datalog {
             step &s = steps[j];
 
             // TBD
-            s.m_labels;
+            // s.m_labels;
 
             // set references, compensate for reverse ordering.
             for (unsigned i = 0; i < s.m_refs.size(); ++i) {
diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp
index a5f8009e7..7a2b47c78 100644
--- a/src/muz_qe/dl_compiler.cpp
+++ b/src/muz_qe/dl_compiler.cpp
@@ -1004,7 +1004,6 @@ namespace datalog {
 
     void compiler::detect_chains(const func_decl_set & preds, func_decl_vector & ordered_preds, 
             func_decl_set & global_deltas) {
-        typedef obj_map<func_decl, func_decl *> pred2pred;
 
         SASSERT(ordered_preds.empty());
         SASSERT(global_deltas.empty());
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index 34513cc76..d8a50668b 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -686,6 +686,7 @@ namespace datalog {
             check_existential_tail(r);
             check_positive_predicates(r);
             break;
+        case LAST_ENGINE:
         default:
             UNREACHABLE();
             break;
@@ -1039,6 +1040,8 @@ namespace datalog {
             case CLP_ENGINE:
                 m_engine = alloc(clp, *this);
                 break;
+            case LAST_ENGINE:
+                UNREACHABLE();
             }
         }
     }
diff --git a/src/muz_qe/dl_mk_array_blast.cpp b/src/muz_qe/dl_mk_array_blast.cpp
index 2c7d3d5cd..9f057a148 100644
--- a/src/muz_qe/dl_mk_array_blast.cpp
+++ b/src/muz_qe/dl_mk_array_blast.cpp
@@ -107,7 +107,6 @@ namespace datalog {
         m_next_var = 0;
         ptr_vector<expr> todo;
         todo.push_back(head);
-        unsigned next_var = 0;
         for (unsigned i = 0; i < conjs.size(); ++i) {
             expr* e = conjs[i].get();
             expr* x, *y;