rename to core2 to avoid overloaded virtual

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

src/muz/spacer/spacer_itp_solver.h

@@ -115,7 +115,7 @@ public:
     virtual void assert_expr_core(expr *t)
     {m_solver.assert_expr(t);}
 
-    virtual void assert_expr_core(expr *t, expr *a)
+    virtual void assert_expr_core2(expr *t, expr *a)
     {NOT_IMPLEMENTED_YET();}
     virtual void assert_lemma(expr* e) { NOT_IMPLEMENTED_YET(); }
     virtual expr_ref lookahead(const expr_ref_vector &,const expr_ref_vector &) { return expr_ref(m.mk_true(), m); }

src/muz/spacer/spacer_virtual_solver.cpp

@@ -50,7 +50,7 @@ virtual_solver::virtual_solver(virtual_solver_factory &factory,
     // -- change m_context, but will add m_pred to
     // -- the private field solver_na2as::m_assumptions
     if (m_virtual)
-    { solver_na2as::assert_expr_core(m.mk_true(), m_pred); }
+    { solver_na2as::assert_expr_core2(m.mk_true(), m_pred); }
 }
 
 virtual_solver::~virtual_solver()

src/sat/sat_lookahead.h

@@ -186,7 +186,7 @@ namespace sat {
                 m_is_decision.reset(); 
                 m_cube.reset(); 
                 m_freevars_threshold = 0;
-                m_psat_threshold = DBL_MAX;
+                m_psat_threshold = 100000000.0;
                 reset_stats();
             }
             void reset_stats() { m_conflicts = 0; m_cutoffs = 0; }

src/sat/sat_solver/inc_sat_solver.cpp

@@ -243,10 +243,10 @@ public:
             --n;
         }
     }
-    virtual unsigned get_scope_level() const {
+    unsigned get_scope_level() const override {
         return m_num_scopes;
     }
-    virtual void assert_expr_core(expr * t, expr * a) {
+    void assert_expr_core2(expr * t, expr * a) override {
         if (a) {
             m_asmsf.push_back(a);
             assert_expr_core(m.mk_implies(a, t));

src/smt/smt_solver.cpp

@@ -105,11 +105,11 @@ namespace smt {
             m_context.assert_expr(t);
         }
 
-        virtual void assert_expr_core(expr * t, expr * a) {
+        virtual void assert_expr_core2(expr * t, expr * a) {
             if (m_name2assertion.contains(a)) {
                 throw default_exception("named assertion defined twice");
             }
-            solver_na2as::assert_expr_core(t, a);
+            solver_na2as::assert_expr_core2(t, a);
             get_manager().inc_ref(t);
             m_name2assertion.insert(a, t);
         }

src/solver/combined_solver.cpp

@@ -172,7 +172,7 @@ public:
             m_solver2->assert_expr(t);
     }
 
-    virtual void assert_expr_core(expr * t, expr * a) {
+    virtual void assert_expr_core2(expr * t, expr * a) {
         if (m_check_sat_executed)
             switch_inc_mode();
         m_solver1->assert_expr(t, a);

src/solver/solver.cpp

@@ -199,7 +199,7 @@ void solver::assert_expr(expr* f, expr* t) {
             // (*mc)(a);        
         }
     }
-    assert_expr_core(fml, a);    
+    assert_expr_core2(fml, a);    
 }
 
 void solver::collect_param_descrs(param_descrs & r) {

src/solver/solver.h

@@ -102,7 +102,7 @@ public:
 
     void assert_expr(expr * t, expr* a);
 
-    virtual void assert_expr_core(expr * t, expr * a) = 0;
+    virtual void assert_expr_core2(expr * t, expr * a) = 0;
 
     /**
        \brief Create a backtracking point.

src/solver/solver_na2as.cpp

@@ -30,9 +30,9 @@ solver_na2as::solver_na2as(ast_manager & m):
 
 solver_na2as::~solver_na2as() {}
 
-void solver_na2as::assert_expr_core(expr * t, expr * a) {
+void solver_na2as::assert_expr_core2(expr * t, expr * a) {
     if (a == 0) {
-        solver::assert_expr_core(t);
+        assert_expr_core(t);
     }
     else {
         SASSERT(is_uninterp_const(a));
@@ -41,7 +41,7 @@ void solver_na2as::assert_expr_core(expr * t, expr * a) {
         m_assumptions.push_back(a);
         expr_ref new_t(m);
         new_t = m.mk_implies(a, t);
-        solver::assert_expr_core(new_t);
+        assert_expr_core(new_t);
     }
 }
 

src/solver/solver_na2as.h

@@ -34,7 +34,7 @@ public:
     solver_na2as(ast_manager & m);
     virtual ~solver_na2as();
 
-    void assert_expr_core(expr * t, expr * a) override;
+    void assert_expr_core2(expr * t, expr * a) override;
     // virtual void assert_expr_core(expr * t) = 0;
     
     // Subclasses of solver_na2as should redefine the following *_core methods instead of these ones.

src/solver/solver_pool.cpp

@@ -49,7 +49,7 @@ public:
         m_in_delayed_scope(false),
         m_dump_counter(0) {
         if (is_virtual()) {
-            solver_na2as::assert_expr_core(m.mk_true(), pred);
+            solver_na2as::assert_expr_core2(m.mk_true(), pred);
         }
     }