avoid crash on nl

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

Author: NikolajBjorner

src/nlsat/nlsat_solver.cpp

@@ -732,7 +732,7 @@ namespace nlsat {
         }
 
         void undo_set_updt(interval_set * old_set) {
-            SASSERT(m_xk != null_var);
+			if (m_xk == null_var) return;
             var x = m_xk;
 			if (x < m_infeasible.size()) {
 				m_ism.dec_ref(m_infeasible[x]);
@@ -741,8 +741,7 @@ namespace nlsat {
         }
 
         void undo_new_stage() {
-            SASSERT(m_xk != null_var);
-            if (m_xk == 0) {
+            if (m_xk == 0 || m_xk == null_var) {
                 m_xk = null_var;
             }
             else {
@@ -758,7 +757,6 @@ namespace nlsat {
         }
 
         void undo_updt_eq(atom * a) {
-            SASSERT(m_xk != null_var);
 			if (m_var2eq.size() > m_xk)
                 m_var2eq[m_xk] = a; 
         }

src/tactic/portfolio/default_tactic.cpp

@@ -41,8 +41,8 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
                                         cond(mk_is_qflra_probe(), mk_qflra_tactic(m),
                                         cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m),
                                         cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m),
-                                        cond(mk_is_nra_probe(),   mk_nra_tactic(m),
                                         cond(mk_is_lira_probe(),  mk_lira_tactic(m, p),
+                                        cond(mk_is_nra_probe(),   mk_nra_tactic(m),
                                         cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p),
                                         //cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p),
                                              mk_smt_tactic()))))))))))),

src/tactic/smtlogics/quant_tactics.cpp

@@ -24,7 +24,6 @@ Revision History:
 #include "qe/qe_tactic.h"
 #include "qe/qe_lite.h"
 #include "qe/qsat.h"
-#include "qe/nlqsat.h"
 #include "tactic/core/ctx_simplify_tactic.h"
 #include "smt/tactic/smt_tactic.h"
 #include "tactic/core/elim_term_ite_tactic.h"