fix #3846, another bug in eq2bv-tactic

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

src/tactic/arith/eq2bv_tactic.cpp

@@ -152,7 +152,7 @@ public:
     obj_map<expr, expr*>             m_fd;
     obj_map<expr, unsigned>          m_max;
     expr_mark                        m_nonfd;
-    ast_mark                         m_has_eq;
+    expr_mark                        m_has_eq;
     ptr_vector<expr>                 m_todo;
         
     eq2bv_tactic(ast_manager & _m):
@@ -203,7 +203,7 @@ public:
         for (unsigned i = 0; !g->inconsistent() && i < g->size(); i++) {            
             expr_ref   new_curr(m);
             proof_ref  new_pr(m);  
-            expr_ref var(m);
+            app_ref var(m);
             if (is_bound(g->form(i), var) && !m_has_eq.is_marked(var)) {
                 if (m.proofs_enabled()) {
                     new_pr = m.mk_rewrite(g->form(i), m.mk_true());
@@ -312,42 +312,42 @@ public:
         }
     }
 
-    bool is_upper(expr* f, expr_ref& var) {
+    bool is_upper(expr* f, app_ref& var) {
         expr* e1, *e2;
         unsigned k;
         if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) && is_var_const_pair(e1, e2, k)) {
             SASSERT(m_bounds.has_upper(e1));
-            var = e1;
+            var = to_app(e1);
             return true;
         } 
         return false;
     }
 
-    bool is_lower(expr* f, expr_ref& var) {
+    bool is_lower(expr* f, app_ref& var) {
         expr* e1, *e2;
         unsigned k;
         if ((a.is_le(f, e1, e2) || a.is_ge(f, e2, e1)) && is_var_const_pair(e2, e1, k)) {
             SASSERT(m_bounds.has_lower(e2));
-            var = e2;
+            var = to_app(e2);
             return true;
         } 
         return false;
     }
 
 
-    bool is_bound(expr* f, expr_ref& var) {
+    bool is_bound(expr* f, app_ref& var) {
         return is_lower(f, var) || is_upper(f, var);
     }
 
     void mark_has_eq(expr* e) {
         if (is_uninterp_const(e)) {
-            m_has_eq.mark(to_app(e)->get_decl(), true);
+            m_has_eq.mark(e, true);
         }
     }
 
     void collect_fd(expr* f) {
         m_trail.push_back(f);
-        expr_ref var(m);
+        app_ref var(m);
         if (is_bound(f, var)) return;
         m_todo.push_back(f);
         while (!m_todo.empty()) {

src/tactic/bv/bv_bounds_tactic.cpp

@@ -241,64 +241,6 @@ namespace {
             return false;
         }
 
-#if 0
-        expr_set* get_expr_vars(expr* t) {
-            unsigned id = t->get_id();
-            m_expr_vars.reserve(id + 1);
-            expr_set*& entry = m_expr_vars[id];
-            if (entry)
-                return entry;
-
-            expr_set* set = alloc(expr_set);
-            entry = set;
-
-            if (!m_bv.is_numeral(t))
-                set->insert(t, true);
-
-            if (!is_app(t))
-                return set;
-
-            app* a = to_app(t);
-            for (unsigned i = 0; i < a->get_num_args(); ++i) {
-                expr_set* set_arg = get_expr_vars(a->get_arg(i));
-                for (expr_set::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) {
-                    set->insert(I->m_key, true);
-                }
-            }
-            return set;
-        }
-#endif
-
-#if 0
-        expr_cnt* get_expr_bounds(expr* t) {
-            unsigned id = t->get_id();
-            m_bound_exprs.reserve(id + 1);
-            expr_cnt*& entry = m_bound_exprs[id];
-            if (entry)
-                return entry;
-
-            expr_cnt* set = alloc(expr_cnt);
-            entry = set;
-
-            if (!is_app(t))
-                return set;
-
-            interval b;
-            expr* e;
-            if (is_bound(t, e, b)) {
-                set->insert_if_not_there2(e, 0)->get_data().m_value++;
-            }
-
-            app* a = to_app(t);
-            for (unsigned i = 0; i < a->get_num_args(); ++i) {
-                expr_cnt* set_arg = get_expr_bounds(a->get_arg(i));
-                for (expr_cnt::iterator I = set_arg->begin(), E = set_arg->end(); I != E; ++I) {
-                    set->insert_if_not_there2(I->m_key, 0)->get_data().m_value += I->m_value;
-                }
-            }
-            return set;
-        }
-#endif
 
     public:
         bv_bounds_simplifier(ast_manager& m, params_ref const& p) : m(m), m_params(p), m_bv(m) {
@@ -475,15 +417,6 @@ namespace {
                 if (contains(t, v.m_key)) return true;
             }
 
-#if 0
-            expr_set* used_exprs = get_expr_vars(t);
-            for (map::iterator I = m_bound.begin(), E = m_bound.end(); I != E; ++I) {
-                if (contains(t, I->m_key)) return true;
-                if (I->m_value.is_singleton() && used_exprs->contains(I->m_key))
-                    return true;
-            }
-#endif
-
             expr* t1;
             interval b;
             // skip common case: single bound constraint without any context for simplification
@@ -494,13 +427,6 @@ namespace {
             if (contains_bound(t)) {
                 return true;
             }
-#if 0
-            expr_cnt* bounds = get_expr_bounds(t);
-            for (expr_cnt::iterator I = bounds->begin(), E = bounds->end(); I != E; ++I) {
-                if (I->m_value > 1 || m_bound.contains(I->m_key))
-                    return true;
-            }
-#endif
             return false;
         }