fix #3962

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

src/ast/arith_decl_plugin.cpp

@@ -698,6 +698,7 @@ bool arith_recognizers::is_numeral(expr const * n, rational & val, bool & is_int
     return true;
 }
 
+
 bool arith_recognizers::is_irrational_algebraic_numeral(expr const * n) const { 
     return is_app(n) && to_app(n)->is_app_of(m_afid, OP_IRRATIONAL_ALGEBRAIC_NUM); 
 }

src/muz/base/rule_properties.cpp

@@ -19,9 +19,10 @@ Notes:
 --*/
 
 #include "ast/expr_functors.h"
+#include "ast/for_each_expr.h"
+#include "ast/rewriter/th_rewriter.h"
 #include "muz/base/rule_properties.h"
 #include "muz/base/dl_rule_set.h"
-#include "ast/for_each_expr.h"
 #include "muz/base/dl_context.h"
 
 using namespace datalog;
@@ -237,12 +238,22 @@ void rule_properties::operator()(app* n) {
     }
     else if ((m_a.is_mod(n, n1, n2) || m_a.is_div(n, n1, n2) ||
               m_a.is_idiv(n, n1, n2) || m_a.is_rem(n, n1, n2))
-             && (!m_a.is_numeral(n2, r) || r.is_zero())) {
+             && (!evaluates_to_numeral(n2, r) || r.is_zero())) {
         m_uninterp_funs.insert(n->get_decl(), m_rule);
     }
     check_sort(m.get_sort(n));
 }
 
+bool rule_properties::evaluates_to_numeral(expr * n, rational& val) {    
+    if (m_a.is_numeral(n, val))
+        return true;
+    th_rewriter rw(m);
+    expr_ref tmp(n, m);
+    rw(tmp);
+    return m_a.is_numeral(tmp, val);
+}
+
+
 void rule_properties::check_sort(sort* s) {
     sort_size sz = s->get_num_elements();
     if (m_ar.is_array(s) || (!sz.is_finite() && !m_dl.is_rule_sort(s))) {

src/muz/base/rule_properties.h

@@ -53,6 +53,7 @@ namespace datalog {
         void insert(ptr_vector<rule>& rules, rule* r);
         void check_sort(sort* s);
         void visit_rules(expr_sparse_mark& visited, rule_set const& rules);
+        bool evaluates_to_numeral(expr * n, rational& val);
     public:
         rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& is_predicate);
         ~rule_properties();