From c388d99c355451eaf22b98c81b97db0d9056450c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Jun 2021 10:58:47 -0700
Subject: [PATCH] #5324

---
 src/sat/sat_extension.h      |  1 +
 src/sat/sat_local_search.cpp | 11 ++++-------
 src/sat/sat_solver.cpp       |  3 ++-
 src/sat/smt/pb_solver.h      |  1 +
 4 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index b03518065..f35f6a58b 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -128,6 +128,7 @@ namespace sat {
                                 std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)>& pb) {                                
             return false;
         }
+        virtual bool is_pb() { return false; }
     };
 
 };
diff --git a/src/sat/sat_local_search.cpp b/src/sat/sat_local_search.cpp
index 433750369..0b3c2f7c9 100644
--- a/src/sat/sat_local_search.cpp
+++ b/src/sat/sat_local_search.cpp
@@ -380,16 +380,14 @@ namespace sat {
 
         if (m_config.phase_sticky()) {
             unsigned v = 0;
-            for (var_info& vi : m_vars) {
+            for (var_info& vi : m_vars) 
                 vi.m_bias = s.m_phase[v++] ? 98 : 2;
-            }
         }
 
         // copy units
         unsigned trail_sz = s.init_trail_size();
-        for (unsigned i = 0; i < trail_sz; ++i) {
+        for (unsigned i = 0; i < trail_sz; ++i) 
             add_clause(1, s.m_trail.data() + i);
-        }
 
         // copy binary clauses
         {
@@ -410,9 +408,8 @@ namespace sat {
         }
 
         // copy clauses
-        for (clause* c : s.m_clauses) {
+        for (clause* c : s.m_clauses) 
             add_clause(c->size(), c->begin());
-        }
         m_num_non_binary_clauses = s.m_clauses.size();
 
 
@@ -422,7 +419,7 @@ namespace sat {
             [&](unsigned sz, literal const* c, unsigned k) { add_cardinality(sz, c, k); };
         std::function<void(unsigned sz, literal const* c, unsigned const* coeffs, unsigned k)> pb = 
             [&](unsigned sz, literal const* c, unsigned const* coeffs, unsigned k) { add_pb(sz, c, coeffs, k); };
-        if (ext && !ext->extract_pb(card, pb))
+        if (ext && (!ext->is_pb() || !ext->extract_pb(card, pb)))
             throw default_exception("local search is incomplete with extensions beyond PB");
         
         if (_init) {
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 9478c6ee9..13ca17764 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1396,7 +1396,8 @@ namespace sat {
             }
         };
         scoped_ls _ls(*this);
-        if (inconsistent()) return l_false;
+        if (inconsistent()) 
+            return l_false;
         scoped_limits scoped_rl(rlimit());
         SASSERT(m_local_search);
         m_local_search->add(*this);
diff --git a/src/sat/smt/pb_solver.h b/src/sat/smt/pb_solver.h
index a3b75300a..c19facf34 100644
--- a/src/sat/smt/pb_solver.h
+++ b/src/sat/smt/pb_solver.h
@@ -211,6 +211,7 @@ namespace pb {
         unsigned next_id() { return m_constraint_id++; }
         void set_non_learned(constraint& c);
         double get_reward(literal l, sat::ext_justification_idx idx, sat::literal_occs_fun& occs) const override;
+        bool is_pb() override { return true; }
 
         // cardinality
         lbool add_assign(card& c, literal lit);