From f5164d166b234d174794fd5c47112106c6c3e07e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 18 Dec 2019 14:25:18 -0800
Subject: [PATCH] unused / return warnings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/dd/dd_pdd.cpp | 2 ++
 src/sat/sat_binspr.cpp | 3 +--
 2 files changed, 3 insertions(+), 2 deletions(-)

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", 
               {