From d7f2638ecf5d0f2fa95fe442f2109550a9c968a8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 7 Feb 2018 16:03:14 -0800
Subject: [PATCH] reference get_wlist

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/ba_solver.cpp      |  4 ++--
 src/sat/sat_simplifier.cpp | 13 ++++++-------
 2 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index 517bd4593..6486380dd 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1390,7 +1390,7 @@ namespace sat {
                     }
                 }
                 else {
-                    slack -= abs(coeff);
+                    slack -= std::abs(coeff);
                     m_lemma.push_back(~lit);
                 }
             }
@@ -3655,7 +3655,7 @@ namespace sat {
             m_active_var_set.insert(v);
             literal lit(v, coeff < 0);
             p.m_lits.push_back(lit);
-            p.m_coeffs.push_back(abs(coeff));
+            p.m_coeffs.push_back(std::abs(coeff));
         }
     }
 
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index a18743438..f773b05e7 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -71,11 +71,11 @@ namespace sat {
         finalize();
     }
 
-    inline watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); }
+    watch_list & simplifier::get_wlist(literal l) { return s.get_wlist(l); }
 
-    inline watch_list const & simplifier::get_wlist(literal l) const { return s.get_wlist(l); }
+    watch_list const & simplifier::get_wlist(literal l) const { return s.get_wlist(l); }
 
-    inline bool simplifier::is_external(bool_var v) const { 
+    bool simplifier::is_external(bool_var v) const { 
         return 
             s.is_assumption(v) ||
             (s.is_external(v) && s.is_incremental()) ||
@@ -1317,16 +1317,15 @@ namespace sat {
             m_ala_qhead = 0;
 
             switch (et) {
-            case abce_t:
-            case bce_t:
-                k = model_converter::BLOCK_LIT;
-                break;
             case cce_t:
                 k = model_converter::CCE;
                 break;
             case acce_t:
                 k = model_converter::ACCE;
                 break;
+            default:
+                k = model_converter::BLOCK_LIT;
+                break;
             }
 
             /*