fix #2919

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

src/ast/static_features.cpp

@@ -312,8 +312,10 @@ void static_features::update_core(expr * e) {
             case OP_IDIV:
             case OP_REM:
             case OP_MOD:
-                if (!is_numeral(to_app(e)->get_arg(1), r) || r.is_zero()) 
+                if (!is_numeral(to_app(e)->get_arg(1), r) || r.is_zero()) {
+                    m_num_uninterpreted_functions++;
                     m_num_non_linear++;
+                }
                 break;
             }
         }

src/smt/smt_setup.cpp

@@ -837,10 +837,7 @@ namespace smt {
                 m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
             break;
         case AS_NEW_ARITH:
-            if (st.m_num_non_linear != 0 && st.m_has_int) 
-                m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));
-            else 
-                setup_lra_arith();
+            setup_lra_arith();
             break;
         default:
             m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params));

src/smt/theory_arith_core.h

@@ -39,7 +39,7 @@ namespace smt {
 
     template<typename Ext>
     void theory_arith<Ext>::found_underspecified_op(app * n) {
-        context& ctx = get_context();
+        context& ctx = get_context();        
         m_underspecified_ops.push_back(n);
         ctx.push_trail(push_back_vector<context, ptr_vector<app>>(m_underspecified_ops));
         if (!m_found_underspecified_op) {
@@ -65,6 +65,7 @@ namespace smt {
             e = m_util.mk_power0(n->get_arg(0), n->get_arg(1));
         }
         if (e) {
+            ast_manager& m = get_manager();
             literal lit = mk_eq(e, n, false);
             ctx.mark_as_relevant(lit);
             ctx.assign(lit, nullptr);
@@ -160,6 +161,10 @@ namespace smt {
             case OP_IDIV:
             case OP_REM:
             case OP_MOD:
+            case OP_DIV0:
+            case OP_IDIV0:
+            case OP_REM0:
+            case OP_MOD0:
                 return true;
             default:
                 break;
@@ -3316,8 +3321,8 @@ namespace smt {
               });
         m_factory = alloc(arith_factory, get_manager());
         m.register_factory(m_factory);
-        compute_epsilon();
         if (!m_model_depends_on_computed_epsilon) {
+            compute_epsilon();
             refine_epsilon();
         }
     }

src/smt/theory_arith_nl.h

@@ -659,6 +659,7 @@ rational theory_arith<Ext>::get_value(theory_var v, bool & computed_epsilon) {
     inf_numeral const & val = get_value(v);
     if (!val.get_infinitesimal().is_zero() && !computed_epsilon) {
         compute_epsilon();
+        refine_epsilon();
         computed_epsilon = true;
         m_model_depends_on_computed_epsilon = true;
     }

src/smt/theory_lra.cpp

@@ -468,12 +468,39 @@ class theory_lra::imp {
         }
     }
 
-    void found_not_handled(expr* n) {
-        m_not_handled = n;
+    void found_unsupported(expr* n) {
+        std::cout << "unsupported: " <<  mk_pp(n, m) << "\n";
+        ctx().push_trail(value_trail<context, expr*>(m_not_handled));
+        m_not_handled = n;    
+    }
+
+    void found_underspecified(expr* n) {
         if (is_app(n) && is_underspecified(to_app(n))) {
             TRACE("arith", tout << "Unhandled: " << mk_pp(n, m) << "\n";);
             m_underspecified.push_back(to_app(n));
         }
+        expr* e = nullptr;
+        if (a.is_div(n)) {                
+            e = a.mk_div0(to_app(n)->get_arg(0), to_app(n)->get_arg(1));
+        }
+        else if (a.is_idiv(n)) {                
+            e = a.mk_idiv0(to_app(n)->get_arg(0), to_app(n)->get_arg(1));
+        }
+        else if (a.is_rem(n)) {                
+            e = a.mk_rem0(to_app(n)->get_arg(0), to_app(n)->get_arg(1));
+        }
+        else if (a.is_mod(n)) {                
+            e = a.mk_mod0(to_app(n)->get_arg(0), to_app(n)->get_arg(1));
+        }
+        else if (a.is_power(n)) {                
+            e = a.mk_power0(to_app(n)->get_arg(0), to_app(n)->get_arg(1));
+        }
+        if (e) {
+            literal lit = th.mk_eq(e, n, false);
+            ctx().mark_as_relevant(lit);
+            ctx().assign(lit, nullptr);
+        }
+
     }
 
     bool is_numeral(expr* term, rational& r) {
@@ -584,7 +611,7 @@ class theory_lra::imp {
                     // already handled
                 }
                 else if (a.is_idiv(n, n1, n2)) {
-                    if (!a.is_numeral(n2, r) || r.is_zero()) found_not_handled(n);
+                    if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
                     m_idiv_terms.push_back(n);
                     app * mod = a.mk_mod(n1, n2);
                     ctx().internalize(mod, false);
@@ -594,18 +621,18 @@ class theory_lra::imp {
                     if (!ctx().relevancy()) mk_idiv_mod_axioms(n1, n2);                    
                 }
                 else if (a.is_rem(n, n1, n2)) {
-                    if (!a.is_numeral(n2, r) || r.is_zero()) found_not_handled(n);
+                    if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
                     if (!ctx().relevancy()) mk_rem_axiom(n1, n2);                    
                 }
                 else if (a.is_div(n, n1, n2)) {
-                    if (!a.is_numeral(n2, r) || r.is_zero()) found_not_handled(n);
+                    if (!a.is_numeral(n2, r) || r.is_zero()) found_underspecified(n);
                     if (!ctx().relevancy()) mk_div_axiom(n1, n2);                    
                 }
-                else if (a.is_power(n)) {
-                    found_not_handled(n);
+                else if (!a.is_div0(n) && !a.is_mod0(n) && !a.is_idiv0(n) && !a.is_rem0(n)) {
+                    found_unsupported(n);
                 }
                 else {
-                    found_not_handled(n);
+                    // no-op
                 }
             }
             else {
@@ -709,6 +736,10 @@ class theory_lra::imp {
             case OP_IDIV:
             case OP_REM:
             case OP_MOD:
+            case OP_DIV0:
+            case OP_IDIV0:
+            case OP_REM0:
+            case OP_MOD0:
                 return true;
             default:
                 break;
@@ -1012,7 +1043,7 @@ public:
         }
         else {
             TRACE("arith", tout << "Could not internalize " << mk_pp(atom, m) << "\n";);
-            found_not_handled(atom);
+            found_unsupported(atom);
             return true;
         }
         if (is_int(v) && !r.is_int()) {