diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 74fe48650..cc926484c 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -17,6 +17,7 @@ Notes:
 
 --*/
 
+#include <typeinfo>
 #include "maxsmt.h"
 #include "fu_malik.h"
 #include "core_maxsat.h"
diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp
index d9b99057f..ef11b8b91 100644
--- a/src/opt/opt_solver.cpp
+++ b/src/opt/opt_solver.cpp
@@ -18,6 +18,7 @@ Notes:
     Based directly on smt_solver.
    
 --*/
+#include <typeinfo>
 #include "reg_decl_plugins.h"
 #include "opt_solver.h"
 #include "smt_context.h"
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index 867273aed..14e133a70 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -37,7 +37,7 @@ Notes:
 
 --*/
 
-
+#include <typeinfo>
 #include "optsmt.h"
 #include "opt_solver.h"
 #include "arith_decl_plugin.h"
diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp
index 84c5e54b8..2a1230656 100644
--- a/src/opt/weighted_maxsat.cpp
+++ b/src/opt/weighted_maxsat.cpp
@@ -16,6 +16,7 @@ Notes:
 
 --*/
 
+#include <typeinfo>
 #include "weighted_maxsat.h"
 #include "smt_theory.h"
 #include "smt_context.h"
@@ -779,7 +780,10 @@ namespace opt {
             }
             lbool is_sat = l_true;
             bool was_sat = false;
+            fml = m.mk_true();
             while (l_true == is_sat) {
+                solver::scoped_push _s(s);
+                s.assert_expr(fml);
                 is_sat = s.check_sat_core(0,0);
                 if (m_cancel) {
                     is_sat = l_undef;
@@ -796,7 +800,6 @@ namespace opt {
                     }                    
                     IF_VERBOSE(1, verbose_stream() << "(wmaxsat.pb with upper bound: " << m_upper << ")\n";);
                     fml = m.mk_not(u.mk_ge(nsoft.size(), m_weights.c_ptr(), nsoft.c_ptr(), m_upper));
-                    s.assert_expr(fml);
                     was_sat = true;
                 }
             }            
diff --git a/src/smt/theory_opt.cpp b/src/smt/theory_opt.cpp
index e6c1ce57f..279863885 100644
--- a/src/smt/theory_opt.cpp
+++ b/src/smt/theory_opt.cpp
@@ -55,7 +55,9 @@ namespace smt {
                 else if (is_numeral(a, t2)) {
                     todo.push_back(t1);
                 }
-                return false;
+                else {
+                    return false;
+                }
             }
             else {
                 return false;
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index f0ea8f6e6..fa9810fc5 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -18,6 +18,7 @@ Notes:
 
 --*/
 
+#include <typeinfo>
 #include "theory_pb.h"
 #include "smt_context.h"
 #include "ast_pp.h"
diff --git a/src/util/scoped_numeral_vector.h b/src/util/scoped_numeral_vector.h
index 585bfa895..f982a7cae 100644
--- a/src/util/scoped_numeral_vector.h
+++ b/src/util/scoped_numeral_vector.h
@@ -47,7 +47,7 @@ public:
     }
 
     void pop_back() {
-        shrink(size()-1);
+        shrink(this->size()-1);
     }
 
     void shrink(unsigned sz) {
diff --git a/tests/chat1.smt2 b/tests/chat1.smt2
index c4e5f63b9..0b489e192 100644
--- a/tests/chat1.smt2
+++ b/tests/chat1.smt2
@@ -3376,5 +3376,5 @@
 ; :wmaxsat_engine pwmax
  :wmaxsat_engine bvmax
  :print_statistics true
- :timeout 60000
+ :timeout 1200000
 )
diff --git a/tests/chat_pb.smt2 b/tests/chat_pb.smt2
index f876b2535..8f32a6328 100644
--- a/tests/chat_pb.smt2
+++ b/tests/chat_pb.smt2
@@ -3371,10 +3371,12 @@
 (assert-soft |dn([7,Main.main],50)_scc(7)| :weight 2)
 (assert-soft |dn([7,Main.main],54)_scc(7)| :weight 2)
 (assert-soft |dn([7,Main.main],58)_scc(7)| :weight 2)
+(set-option :smt.pb.conflict_frequency 100)
+
 (optimize
 ; :wmaxsat_engine wpm2
  :wmaxsat_engine pwmax
 ; :wmaxsat_engine bvmax
  :print_statistics true
- :timeout 60000
+ :timeout 1200000
 )