debugging Z3Prover#4169

Author: NikolajBjorner

src/smt/smt_context.cpp

@@ -763,7 +763,6 @@ namespace smt {
             // Common case: r2 and r1 have at most one theory var.
             theory_id  t2 = r2->m_th_var_list.get_th_id();
             theory_id  t1 = r1->m_th_var_list.get_th_id();
-            // verbose_stream() << "[merge_theory_vars] t2: " << t2 << ", t1: " << t1 << "\n";
             theory_var v2 = m_fparams.m_new_core2th_eq ? get_closest_var(n2, t2) : r2->m_th_var_list.get_th_var();
             theory_var v1 = m_fparams.m_new_core2th_eq ? get_closest_var(n1, t1) : r1->m_th_var_list.get_th_var();
             TRACE("merge_theory_vars",
@@ -1422,8 +1421,8 @@ namespace smt {
             TRACE("push_new_th_diseqs", tout << m.get_family_name(th->get_id()) << " not using diseqs\n";);
             return;
         }
-        TRACE("push_new_th_diseqs", tout << "#" << r->get_owner_id() << " v" << v << "\n";);
         theory_id th_id = th->get_id();
+        TRACE("push_new_th_diseqs", tout << "#" << r->get_owner_id() << " " << mk_bounded_pp(r->get_owner(), m) << " v" << v << " th: " << th_id << "\n";);
         for (enode * parent : r->get_parents()) {
             CTRACE("parent_bug", parent == 0, tout << "#" << r->get_owner_id() << ", num_parents: " << r->get_num_parents() << "\n"; display(tout););
             if (parent->is_eq()) {
@@ -1601,6 +1600,11 @@ namespace smt {
             if (inconsistent())
                 return false;
         }
+#if 0
+        if (at_search_level() && induction::should_try(*this)) {
+            get_induction()();
+        }
+#endif
         return true;
     }
 

src/smt/smt_context_inv.cpp

@@ -291,8 +291,6 @@ namespace smt {
                                 if (eq.m_th_id == th_id) {
                                     enode * lhs_prime = th->get_enode(eq.m_lhs)->get_root();
                                     enode * rhs_prime = th->get_enode(eq.m_rhs)->get_root();
-                                    TRACE("check_th_diseq_propagation", 
-                                          tout << m.get_family_name(eq.m_th_id) << "\n";);
 
                                     if ((lhs == lhs_prime && rhs == rhs_prime) ||
                                         (rhs == lhs_prime && lhs == rhs_prime)) {
@@ -302,15 +300,13 @@ namespace smt {
                                     }
                                 }
                             }
-                            if (!found) {
-                            // missed theory diseq propagation
-                                display(std::cout);
-                                std::cout << "checking theory: " << m.get_family_name(th_id) << "\n";
-                                std::cout << "root: #" << n->get_root()->get_owner_id() << " node: #" << n->get_owner_id() << "\n";
-                                std::cout << mk_pp(n->get_owner(), m) << "\n";
-                                std::cout << "lhs: #" << lhs->get_owner_id() << ", rhs: #" << rhs->get_owner_id() << "\n";
-                                std::cout << mk_bounded_pp(lhs->get_owner(), m) << " " << mk_bounded_pp(rhs->get_owner(), m) << "\n";
-                            }
+                            CTRACE("check_th_diseq_propagation", !found,
+                                   tout 
+                                   << "checking theory: " << m.get_family_name(th_id) << "\n"
+                                   << "root: #" << n->get_root()->get_owner_id() << " node: #" << n->get_owner_id() << "\n"
+                                   << mk_pp(n->get_owner(), m) << "\n"
+                                   << "lhs: #" << lhs->get_owner_id() << ", rhs: #" << rhs->get_owner_id() << "\n"
+                                   << mk_bounded_pp(lhs->get_owner(), m) << " " << mk_bounded_pp(rhs->get_owner(), m) << "\n";);
                             VERIFY(found);
                         }
                         l = l->get_next();

src/smt/theory_array.cpp

@@ -312,12 +312,14 @@ namespace smt {
 
     void theory_array::new_diseq_eh(theory_var v1, theory_var v2) {
         v1 = find(v1);
-        v2 = find(v2);
+        v2 = find(v2);        
         var_data * d1 = m_var_data[v1];
+        TRACE("ext", tout << "extensionality: " << d1->m_is_array << "\n" 
+              << mk_bounded_pp(get_enode(v1)->get_owner(), get_manager(), 5) << "\n" 
+              << mk_bounded_pp(get_enode(v2)->get_owner(), get_manager(), 5) << "\n";);
+        
         if (d1->m_is_array) {
             SASSERT(m_var_data[v2]->m_is_array);
-            TRACE("ext", tout << "extensionality:\n" << mk_bounded_pp(get_enode(v1)->get_owner(), get_manager(), 5) << "\n" << 
-                  mk_bounded_pp(get_enode(v2)->get_owner(), get_manager(), 5) << "\n";);
             instantiate_extensionality(get_enode(v1), get_enode(v2));
         }
     }