fix compilation errors

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/opt/maxsmt.cpp

@@ -17,6 +17,7 @@ Notes:
 
 --*/
 
+#include <typeinfo>
 #include "maxsmt.h"
 #include "fu_malik.h"
 #include "core_maxsat.h"

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"

src/opt/optsmt.cpp

@@ -37,7 +37,7 @@ Notes:
 
 --*/
 
-
+#include <typeinfo>
 #include "optsmt.h"
 #include "opt_solver.h"
 #include "arith_decl_plugin.h"

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;
                 }
             }            

src/smt/theory_opt.cpp

@@ -55,8 +55,10 @@ namespace smt {
                 else if (is_numeral(a, t2)) {
                     todo.push_back(t1);
                 }
+                else {
                     return false;
                 }
+            }
             else {
                 return false;
             } 

src/smt/theory_pb.cpp

@@ -18,6 +18,7 @@ Notes:
 
 --*/
 
+#include <typeinfo>
 #include "theory_pb.h"
 #include "smt_context.h"
 #include "ast_pp.h"

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) {

tests/chat1.smt2

@@ -3376,5 +3376,5 @@
 ; :wmaxsat_engine pwmax
  :wmaxsat_engine bvmax
  :print_statistics true
- :timeout 60000
+ :timeout 1200000
 )

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
 )