bugfixes

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

src/sat/smt/arith_axioms.cpp

@@ -547,6 +547,7 @@ namespace arith {
     }
 
     void solver::new_diseq_eh(euf::th_eq const& e) {
+        TRACE("artih", tout << mk_bounded_pp(e.eq(), m) << "\n");
         ensure_column(e.v1());
         ensure_column(e.v2());
         m_delayed_eqs.push_back(std::make_pair(e, false));

src/sat/smt/arith_solver.cpp

@@ -987,10 +987,10 @@ namespace arith {
     }
 
     bool solver::use_nra_model() {
-        return m_nla && m_nla->use_nra_model();
+        return m_nla && m_use_nra_model && m_nla->use_nra_model();
     }
 
-    bool solver::is_eq(theory_var v1, theory_var v2) {
+    bool solver::is_eq(theory_var v1, theory_var v2) {        
         if (use_nra_model()) {
             return m_nla->am().eq(nl_value(v1, m_nla->tmp1()), nl_value(v2, m_nla->tmp2()));
         }
@@ -1005,6 +1005,8 @@ namespace arith {
         IF_VERBOSE(12, verbose_stream() << "final-check " << lp().get_status() << "\n");
         SASSERT(lp().ax_is_correct());
 
+        m_use_nra_model = false;
+
         if (!lp().is_feasible() || lp().has_changed_columns()) {
             switch (make_feasible()) {
             case l_false:
@@ -1042,6 +1044,7 @@ namespace arith {
 
         switch (check_nla()) {
         case l_true:
+            m_use_nra_model = true;
             break;
         case l_false:
             return sat::check_result::CR_CONTINUE;
@@ -1056,6 +1059,9 @@ namespace arith {
             return sat::check_result::CR_CONTINUE;
         }
 
+        if (!check_delayed_eqs())
+            return sat::check_result::CR_CONTINUE;
+
         if (!int_undef && !check_bv_terms())
             return sat::check_result::CR_CONTINUE;
 
@@ -1141,6 +1147,7 @@ namespace arith {
                 new_eq_eh(e);
             else if (is_eq(e.v1(), e.v2())) {
                 mk_diseq_axiom(e.v1(), e.v2());
+                TRACE("arith", tout << mk_bounded_pp(e.eq(), m) << " " << use_nra_model() << "\n");
                 found_diseq = true;
                 break;
             }
@@ -1271,9 +1278,10 @@ namespace arith {
                 m_core.push_back(ctx.mk_literal(m.mk_eq(eq.first->get_expr(), eq.second->get_expr())));
             for (literal& c : m_core)
                 c.neg();
-            DEBUG_CODE(for (literal c : m_core) { SASSERT(s().value(c) != l_true); });
 
-            for (literal c : m_core) { VERIFY(s().value(c) != l_true); }
+            // it is possible if multiple lemmas are added at the same time.
+            if (any_of(m_core, [&](literal c) { return s().value(c) == l_true; }))
+                return;
             
             add_redundant(m_core, explain(ty));
         }
@@ -1511,6 +1519,7 @@ namespace arith {
         case l_undef:
             break;
         }
+        TRACE("arith", tout << "nla " << r << "\n");
         return r;
     }
 

src/sat/smt/arith_solver.h

@@ -230,6 +230,7 @@ namespace arith {
 
         // non-linear arithmetic
         scoped_ptr<nla::solver>  m_nla;
+        bool m_use_nra_model = false;
 
         // integer arithmetic
         scoped_ptr<lp::int_solver>   m_lia;

src/sat/smt/sls_solver.cpp

@@ -61,7 +61,7 @@ namespace sls {
     }
 
     void solver::set_finished() {
-        m.limit().cancel();
+        ctx.s().set_canceled();
     }
 
     unsigned solver::get_num_bool_vars() const {

src/smt/smt_context.cpp

@@ -104,8 +104,10 @@ namespace smt {
     */
 
     bool context::get_cancel_flag() {
-        if (l_true == m_sls_completed)
+        if (l_true == m_sls_completed && !m.limit().suspended()) {
+            m_last_search_failure = CANCELED;
             return true;
+        }
         if (m.limit().inc())
             return false;
         m_last_search_failure = CANCELED;
@@ -3506,11 +3508,10 @@ namespace smt {
               m_case_split_queue->display(tout << "case splits\n");
               );
         display_profile(verbose_stream());
-        if (r == l_true && get_cancel_flag()) {
+        if (r == l_true && get_cancel_flag()) 
             r = l_undef;
-        }
         if (r == l_undef && m_sls_completed == l_true && has_sls_model()) {
-            m.limit().reset_cancel();
+            m_last_search_failure = OK;
             r = l_true;
         }
         m_sls_completed = l_false;

src/smt/theory_sls.cpp

@@ -38,11 +38,12 @@ namespace smt {
     }
     
     void theory_sls::initialize_value(expr* t, expr* v) {
-        ctx.user_propagate_initialize_value(t, v);
+        //ctx.user_propagate_initialize_value(t, v);
     }
     
     void theory_sls::force_phase(sat::literal lit) {
-        ctx.force_phase(lit);
+        //
+        //        ctx.force_phase(lit);
     }
     
     void theory_sls::set_has_new_best_phase(bool b) {
@@ -108,7 +109,7 @@ namespace smt {
 
 #endif
         
-        m_smt_plugin->import_from_sls();        
+        //        m_smt_plugin->import_from_sls();        
     }       
 
     void theory_sls::init() {