fix 3838 fix #3837

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

src/ast/ast.cpp

@@ -1800,7 +1800,7 @@ static void track_id(ast* n, unsigned id) {
     if (n->get_id() != id) return;
     ++s_count;
     std::cout << s_count << "\n";
-    //SASSERT(s_count != 2);
+    SASSERT(s_count != 1);
 }
 #endif
 
@@ -1834,7 +1834,7 @@ ast * ast_manager::register_node_core(ast * n) {
 
     n->m_id = is_decl(n) ? m_decl_id_gen.mk() : m_expr_id_gen.mk();
 
-    // track_id(n, 48);
+    //    track_id(n, 323);
 
     TRACE("ast", tout << "Object " << n->m_id << " was created.\n";);
     TRACE("mk_var_bug", tout << "mk_ast: " << n->m_id << "\n";);
@@ -2902,8 +2902,8 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2) {
               (is_eq(get_fact(p2)) || is_oeq(get_fact(p2)))));
     CTRACE("mk_transitivity", to_app(get_fact(p1))->get_arg(1) != to_app(get_fact(p2))->get_arg(0),
            tout << mk_pp(get_fact(p1), *this) << "\n\n" << mk_pp(get_fact(p2), *this) << "\n";
-           tout << mk_bounded_pp(p1, *this, 5) << "\n\n";
+           tout << p1->get_id() << ": " << mk_bounded_pp(p1, *this, 5) << "\n\n";
-           tout << mk_bounded_pp(p2, *this, 5) << "\n\n";
+           tout << p2->get_id() << ": " << mk_bounded_pp(p2, *this, 5) << "\n\n";
     );
     SASSERT(to_app(get_fact(p1))->get_arg(1) == to_app(get_fact(p2))->get_arg(0));
     if (is_reflexivity(p1))
@@ -2913,7 +2913,10 @@ proof * ast_manager::mk_transitivity(proof * p1, proof * p2) {
     // OEQ is compatible with EQ for transitivity.
     func_decl* f = to_app(get_fact(p1))->get_decl();
     if (is_oeq(get_fact(p2))) f = to_app(get_fact(p2))->get_decl();
-    return mk_app(m_basic_family_id, PR_TRANSITIVITY, p1, p2, mk_app(f, to_app(get_fact(p1))->get_arg(0), to_app(get_fact(p2))->get_arg(1)));
+    proof* p = mk_app(m_basic_family_id, PR_TRANSITIVITY, p1, p2, mk_app(f, to_app(get_fact(p1))->get_arg(0), to_app(get_fact(p2))->get_arg(1)));
+
+//    SASSERT(p->get_id() != 202);
+    return p;
 }
 
 proof * ast_manager::mk_transitivity(proof * p1, proof * p2, proof * p3) {
@@ -2955,7 +2958,9 @@ proof * ast_manager::mk_monotonicity(func_decl * R, app * f1, app * f2, unsigned
     ptr_buffer<expr> args;
     args.append(num_proofs, (expr**) proofs);
     args.push_back(mk_app(R, f1, f2));
-    return mk_app(m_basic_family_id, PR_MONOTONICITY, args.size(), args.c_ptr());
+    proof* p = mk_app(m_basic_family_id, PR_MONOTONICITY, args.size(), args.c_ptr());
+    SASSERT(p->get_id() != 202);
+    return p;
 }
 
 proof * ast_manager::mk_congruence(app * f1, app * f2, unsigned num_proofs, proof * const * proofs) {

src/ast/rewriter/rewriter_def.h

@@ -184,6 +184,7 @@ bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
         if (to_app(t)->get_num_args() == 0) {
             if (process_const<ProofGen>(to_app(t))) 
                 return true; 
+            TRACE("rewriter", tout << "process const: " << mk_bounded_pp(t, m()) << " -> " << mk_bounded_pp(m_r,m()) << "\n";);
             t = m_r;
         }
         if (max_depth != RW_UNBOUNDED_DEPTH)
@@ -302,6 +303,7 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
                if (m_pr2) tout << mk_bounded_pp(m_pr2, m()) << "\n";
               );
         SASSERT(st == BR_FAILED || rewrites_to(m_r, m_pr2));
+        SASSERT(st == BR_FAILED || rewrites_from(new_t, m_pr2));
         SASSERT(st != BR_DONE || m().get_sort(m_r) == m().get_sort(t));
         if (st != BR_FAILED) {
             result_stack().shrink(fr.m_spos);
@@ -314,6 +316,8 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
                 m_pr  = m().mk_transitivity(m_pr, m_pr2);
                 m_pr2 = nullptr;
                 result_pr_stack().push_back(m_pr);
+                SASSERT(rewrites_to(m_r, m_pr));
+                SASSERT(rewrites_from(t, m_pr));
             }
             if (st == BR_DONE) {
                 cache_result<ProofGen>(t, m_r, m_pr, fr.m_cache_result);
@@ -346,6 +350,8 @@ void rewriter_tpl<Config>::process_app(app * t, frame & fr) {
                         result_pr_stack().push_back(m_pr);
                     }
                     m_r = result_stack().back();
+                    SASSERT(rewrites_to(m_r, m_pr));
+                    SASSERT(rewrites_from(t, m_pr));
                     result_stack().pop_back();
                     result_stack().pop_back();
                     result_stack().push_back(m_r);

src/muz/base/hnf.cpp

@@ -165,10 +165,7 @@ public:
             }
         }
         TRACE("hnf",
-              tout << mk_pp(n, m) << "\n==>\n";
+            tout << mk_pp(n, m) << "\n==>\n" << result << "\n";);
-              for (unsigned i = 0; i < result.size(); ++i) {
-                  tout << mk_pp(result[i].get(), m) << "\n";
-              });
     }
 
     bool checkpoint() {
@@ -458,13 +455,13 @@ private:
     }
 
 
-    proof_ref mk_congruence(proof* p1, expr_ref_vector const& body, expr* head, proof_ref_vector& defs) {
+    proof_ref mk_congruence(proof* p, expr_ref_vector const& body, expr* head, proof_ref_vector& defs) {
         if (defs.empty()) {
-            return proof_ref(p1, m);
+            return proof_ref(p, m);
         }
         else {
-            SASSERT(p1);
+            SASSERT(p);
-            proof_ref p2(m), p3(m);
+            proof_ref p1(p, m), p2(m), p3(m);
             app_ref fml = mk_implies(body, head);
             expr* fact = m.get_fact(p1);
             if (m.is_iff(fact)) {

src/muz/fp/horn_tactic.cpp

@@ -349,15 +349,19 @@ class horn_tactic : public tactic {
         void check_parameters() {
             fp_params const& p = m_ctx.get_params();
             if (p.engine() == symbol("datalog"))
-                not_supported();
+                not_supported("engine=datalog");
             if (p.datalog_generate_explanations())
-                not_supported(); 
+                not_supported("datalog.generate_explanations"); 
             if (p.datalog_magic_sets_for_queries())
-                not_supported();
+                not_supported("datalog.magic_sets_for_queries");
+            if (p.xform_instantiate_arrays())
+                not_supported("xform.instantiate_arrays");
+            if (p.xform_magic())
+                not_supported("xform.magic");
         }
 
-        void not_supported() {
+        void not_supported(char const* s) {
-            throw default_exception("unsupported parameter combination passed to HORN tactic");
+            throw default_exception(std::string("unsupported parameter ") + s);
         }
 
     };