From a261bd94ed3c5b3f2bbce510b2ec52337f168b84 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Fri, 10 Apr 2020 15:19:57 -0400
Subject: [PATCH] silence #3788

better proof generation for the case when the query is reachable from initial
states. This case needs to be handled better so that spacer can assume
the problem is non-trivial.
---
 src/muz/spacer/spacer_context.cpp    | 39 +++++++++++++++-------------
 src/muz/spacer/spacer_context.h      |  2 +-
 src/muz/spacer/spacer_sat_answer.cpp |  5 ++--
 3 files changed, 25 insertions(+), 21 deletions(-)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 657668c49..71579cd2b 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1004,19 +1004,19 @@ app_ref pred_transformer::mk_fresh_rf_tag ()
     return app_ref(m.mk_const (pm.get_n_pred (decl)), m);
 }
 
-void pred_transformer::add_rf (reach_fact *rf)
+void pred_transformer::add_rf (reach_fact *rf, bool force)
 {
     timeit _timer (is_trace_enabled("spacer_timeit"),
                    "spacer::pred_transformer::add_rf",
                    verbose_stream ());
 
-    TRACE ("spacer",
-           tout << "add_rf: " << head()->get_name() << " "
-           << (rf->is_init () ? "INIT " : "")
-           << mk_pp(rf->get (), m) << "\n";);
+    if (!rf) return;
+    TRACE("spacer", tout << "add_rf: " << head()->get_name() << " "
+                         << (rf->is_init() ? "INIT " : "")
+                         << mk_pp(rf->get(), m) << "\n";);
 
-    // -- avoid duplicates
-    if (!rf || get_rf(rf->get())) {return;}
+    // -- avoid duplicates unless forced
+    if (!force && get_rf(rf->get())) {return;}
 
     // all initial facts are grouped together
     SASSERT (!rf->is_init () || m_reach_facts.empty () ||
@@ -1384,7 +1384,11 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
         if (model && model->get()) {
             r = find_rule(**model, is_concrete, reach_pred_used, num_reuse_reach);
             TRACE("spacer", 
-                tout << "reachable " << r << " is_concrete " << is_concrete << " rused: " << reach_pred_used << "\n";);
+                  tout << "reachable is_sat: " << is_sat << " "
+                  << r << " is_concrete " << is_concrete << " rused: " << reach_pred_used << "\n";
+                  ctx.get_datalog_context().get_rule_manager().display_smt2(*r, tout) << "\n";
+                  );
+            TRACE("spacer_sat", tout << "model is:\n" << **model << "\n";);
         }
 
         return is_sat;
@@ -1392,13 +1396,7 @@ lbool pred_transformer::is_reachable(pob& n, expr_ref_vector* core,
     if (is_sat == l_false) {
         SASSERT (reach_assumps.empty ());
         TRACE ("spacer", tout << "unreachable with lemmas\n";
-               if (core) {
-                   tout << "Core:\n";
-                   for (unsigned i = 0; i < core->size (); i++) {
-                       tout << mk_pp (core->get(i), m) << "\n";
-                   }
-               }
-            );
+               if (core) tout << "Core:\n" << *core << "\n";);
         uses_level = m_solver->uses_level();
         return l_false;
     }
@@ -3378,10 +3376,15 @@ lbool context::expand_pob(pob& n, pob_ref_buffer &out)
         // must-reachable
         if (is_concrete) {
             // -- update must summary
-            if (r && r->get_uninterpreted_tail_size() > 0) {
-                reach_fact_ref rf = n.pt().mk_rf (n, *model, *r);
+            CTRACE("spacer_sat", r,
+                   tout << "Concrete reachable with a rule:\n";
+                   get_datalog_context().get_rule_manager().display_smt2(*r, tout) << "\n";
+                   );
+            bool is_root = m_pob_queue.is_root(n);
+            if (r && (r->get_uninterpreted_tail_size() > 0 || is_root )) {
+                reach_fact_ref rf = n.pt().mk_rf(n, *model, *r);
                 checkpoint ();
-                n.pt ().add_rf (rf.get ());
+                n.pt ().add_rf(rf.get (), is_root);
                 checkpoint ();
             }
 
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 2e4a63474..89fac2225 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -510,7 +510,7 @@ public:
     /// initialize reachability facts using initial rules
     void init_rfs ();
     reach_fact *mk_rf(pob &n, model &mdl, const datalog::rule &r);
-    void add_rf (reach_fact *fact);  // add reachability fact
+    void add_rf (reach_fact *fact, bool force = false);  // add reachability fact
     reach_fact* get_last_rf () const { return m_reach_facts.back (); }
     expr* get_last_rf_tag () const;
 
diff --git a/src/muz/spacer/spacer_sat_answer.cpp b/src/muz/spacer/spacer_sat_answer.cpp
index 98e93be1d..5438436e3 100644
--- a/src/muz/spacer/spacer_sat_answer.cpp
+++ b/src/muz/spacer/spacer_sat_answer.cpp
@@ -64,8 +64,9 @@ proof_ref ground_sat_answer_op::operator()(pred_transformer &query) {
         solver::scoped_push _s_(*m_solver);
         m_solver->assert_expr(query.get_last_rf()->get());
         lbool res = m_solver->check_sat(0, nullptr);
-        (void)res;
-        SASSERT(res == l_true);
+        CTRACE("spacer_sat", res != l_true, tout << "solver at check:\n";
+               m_solver->display(tout) << "res: " << res << "\n";);
+        VERIFY(res == l_true);
         model_ref mdl;
         m_solver->get_model(mdl);
         mdl->compress();