patching can break monomials, so rerun nla

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

src/ast/simplifiers/bound_simplifier.cpp

@@ -58,9 +58,9 @@ struct bound_simplifier::rw : public rewriter_tpl<rw_cfg> {
 br_status bound_simplifier::reduce_app(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result, proof_ref& pr) {
     rational N, hi, lo;
     if (a.is_mod(f) && num_args == 2 && a.is_numeral(args[1], N)) {
-        expr* x = args[0];
         auto& im = m_interval;
         scoped_dep_interval i(im);
+        expr* x = args[0];
         get_bounds(x, i);
         if (im.upper_is_inf(i) || im.lower_is_inf(i))
             return BR_FAILED;
@@ -83,7 +83,55 @@ br_status bound_simplifier::reduce_app(func_decl* f, unsigned num_args, expr* co
         }
         IF_VERBOSE(2, verbose_stream() << "potentially missed simplification: " << mk_pp(x, m) << " " << lo << " " << hi << " not reduced\n");
     }
-    return BR_FAILED;
+
+    expr_ref_buffer new_args(m);
+    expr_ref new_arg(m);
+    bool change = false;
+    for (unsigned i = 0; i < num_args; ++i) {
+        expr* arg = args[i];
+        change = reduce_arg(arg, new_arg) || change;
+        new_args.push_back(new_arg);
+    }
+    if (!change)
+        return BR_FAILED;
+
+    result = m.mk_app(f, num_args, new_args.data());
+
+    return BR_DONE;
+}
+
+bool bound_simplifier::reduce_arg(expr* arg, expr_ref& result) {
+    result = arg;
+    expr* x, *y;
+    rational N, lo, hi;
+    bool strict;
+    if ((a.is_le(arg, x, y) && a.is_numeral(y, N)) ||
+        (a.is_ge(arg, y, x) && a.is_numeral(y, N))) {
+
+        if (has_upper(x, hi, strict) && !strict && N >= hi) {
+            result = m.mk_true();
+            return true;
+        }
+        if (has_lower(x, lo, strict) && !strict && N < lo) {
+            result = m.mk_false();
+            return true;
+        }
+        return false;
+    }
+    
+    if ((a.is_le(arg, y, x) && a.is_numeral(y, N)) ||
+        (a.is_ge(arg, x, y) && a.is_numeral(y, N))) {
+        if (has_lower(x, lo, strict) && !strict && N <= lo) {
+            result = m.mk_true();
+            return true;
+        }
+        if (has_upper(x, hi, strict) && !strict && N > hi) {
+            result = m.mk_false();
+            return true;
+        }
+        return false;
+    }
+    return false;
 }
 
 void bound_simplifier::reduce() {

src/ast/simplifiers/bound_simplifier.h

@@ -77,8 +77,12 @@ class bound_simplifier : public dependent_expr_simplifier {
         return v;
     }
 
+    bool reduce_arg(expr* arg, expr_ref& result);
+
     br_status reduce_app(func_decl* f, unsigned num_args, expr* const* args, expr_ref& result, proof_ref& pr);
 
+    
+
     void assert_lower(expr* x, rational const& n, bool strict);
     void assert_upper(expr* x, rational const& n, bool strict);
 

src/smt/theory_arith_core.h

@@ -416,8 +416,9 @@ namespace smt {
             unsigned r_id = mk_row();
             scoped_row_vars _sc(m_row_vars, m_row_vars_top);
             check_app(arg1, m);
-            if (reflection_enabled())
+            if (reflection_enabled()) {
                 internalize_term_core(to_app(arg0));
+            }
             theory_var v = internalize_mul_core(to_app(arg1));
             add_row_entry<true>(r_id, val, v);
             enode * e      = mk_enode(m);
@@ -1535,6 +1536,9 @@ namespace smt {
                 TRACE("arith", tout << "assume_eqs(), ok: " << ok << "\n";);
                 break;
             default:
+                TRACE("arith", ctx.display(tout));
+                ctx.display(verbose_stream());
+                exit(0);
                 ok = process_non_linear();
                 TRACE("arith", tout << "non_linear(), ok: " << ok << "\n";);
                 break;

src/smt/theory_lra.cpp

@@ -2252,6 +2252,9 @@ public:
                     // verbose_stream() << "not done\n";
                     return FC_CONTINUE;
                 }
+                st = check_nla();
+                if (st != FC_DONE)
+                    return st;
 
             }
             return st;