diff --git a/src/math/dd/dd_pdd.cpp b/src/math/dd/dd_pdd.cpp
index 9b38424a4..88a91e764 100644
--- a/src/math/dd/dd_pdd.cpp
+++ b/src/math/dd/dd_pdd.cpp
@@ -81,6 +81,7 @@ namespace dd {
             }
         }
         SASSERT(well_formed());
+        return 0;
     }
 
     bool pdd_manager::check_result(op_entry*& e1, op_entry const* e2, PDD a, PDD b, PDD c) {
@@ -231,6 +232,7 @@ namespace dd {
             }
         }
         SASSERT(well_formed());        
+        return pdd(zero_pdd, this);
     }
 
     pdd_manager::PDD pdd_manager::minus_rec(PDD a) {
diff --git a/src/sat/sat_binspr.cpp b/src/sat/sat_binspr.cpp
index c73dab168..89826cd38 100644
--- a/src/sat/sat_binspr.cpp
+++ b/src/sat/sat_binspr.cpp
@@ -155,7 +155,7 @@ namespace sat {
             p.set_uint("sat.max_conflicts", 10000);
             p.set_bool("sat.binspr", false);
             s->updt_params(p);
-            lbool r = s->check(0, nullptr);
+            s->check(0, nullptr);
         }
 
         if (s->inconsistent()) {
@@ -422,7 +422,6 @@ namespace sat {
                 break;
             }
         }
-        bool first = m_state == ~0;
         m_state &= mask;
         TRACE("sat", 
               {