mask regression

src/ast/bv_decl_plugin.cpp

@@ -651,9 +651,9 @@ void bv_decl_plugin::get_offset_term(app * a, expr * & t, rational & offset) con
 }
 
 bool bv_decl_plugin::are_distinct(app * a, app * b) const {
-    if (is_value(a) && is_value(b))
-        return a != b;
-#if 1
+    if (decl_plugin::are_distinct(a, b))
+        return true;
+    
     // Check for a + k1 != a + k2   when k1 != k2
     rational a_offset;
     expr *   a_term;
@@ -668,8 +668,7 @@ bool bv_decl_plugin::are_distinct(app * a, app * b) const {
           tout << "b: " << b_offset << " + " << mk_ismt2_pp(b_term, *m_manager) << "\n";);
     if (a_term == b_term && a_offset != b_offset)
         return true;
-#endif
-    return decl_plugin::are_distinct(a, b);
+    return false;    
 }
 
 void bv_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol const & logic) {

src/ast/rewriter/array_rewriter.cpp

@@ -176,10 +176,15 @@ br_status array_rewriter::mk_select_core(unsigned num_args, expr * const * args,
         case l_false: {
             expr* arg0 = args[0];
             expr* arg1 = to_app(arg0)->get_arg(0);
+#if 0
+            IF_VERBOSE(0, verbose_stream() << mk_pp(arg0, m()) << "\n");
             while (m_util.is_store(arg1) && compare_args<true>(num_args-1, args + 1, to_app(arg0)->get_args() + 1) == l_false) {
+                IF_VERBOSE(0, verbose_stream() << "diff: " << mk_pp(arg1, m()) << "\n");
+
                 arg0 = arg1;
                 arg1 = to_app(arg0)->get_arg(0);
             }
+#endif
 
             // select(store(a, I, v), J) --> select(a, J) if I != J
             ptr_buffer<expr> new_args;