From 6f346bf804375fd67dbc73167e8eb8a0cf784528 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 31 Jan 2021 22:56:42 -0800
Subject: [PATCH] fix build break

---
 src/math/lp/nla_core.cpp |  2 --
 src/sat/smt/q_clause.cpp |  8 ++++----
 src/sat/smt/q_clause.h   |  3 +--
 src/sat/smt/q_ematch.cpp | 21 +++++++++++++++++++++
 src/sat/smt/q_ematch.h   |  2 ++
 5 files changed, 28 insertions(+), 8 deletions(-)

diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp
index cba9e13b6..072cd1ac0 100644
--- a/src/math/lp/nla_core.cpp
+++ b/src/math/lp/nla_core.cpp
@@ -1936,5 +1936,3 @@ void core::collect_statistics(::statistics & st) {
 
 } // end of nla
 
-template void nla::intervals::set_var_interval<dd::w_dep::without_deps>(lpvar v, nla::intervals::interval& b);
-template void nla::intervals::set_var_interval<dd::w_dep::with_deps>(lpvar v, nla::intervals::interval& b);
diff --git a/src/sat/smt/q_clause.cpp b/src/sat/smt/q_clause.cpp
index 0e64d5029..0d4049167 100644
--- a/src/sat/smt/q_clause.cpp
+++ b/src/sat/smt/q_clause.cpp
@@ -23,13 +23,13 @@ namespace q {
     std::ostream& lit::display(std::ostream& out) const {
         ast_manager& m = lhs.m();
         if (m.is_true(rhs) && !sign) 
-            return out << lhs;
+            return out << mk_bounded_pp(lhs, m, 2);
         if (m.is_false(rhs) && !sign) 
-            return out << "(not " << lhs << ")";
+            return out << "(not " << mk_bounded_pp(lhs, m, 2) << ")";
         return 
-            out << mk_bounded_pp(lhs, lhs.m(), 2) 
+            out << mk_bounded_pp(lhs, m, 2) 
                 << (sign ? " != " : " == ") 
-                << mk_bounded_pp(rhs, rhs.m(), 2);
+                << mk_bounded_pp(rhs, m, 2);
     }
 
     std::ostream& clause::display(euf::solver& ctx, std::ostream& out) const {
diff --git a/src/sat/smt/q_clause.h b/src/sat/smt/q_clause.h
index 823263964..6cdf2a8f4 100644
--- a/src/sat/smt/q_clause.h
+++ b/src/sat/smt/q_clause.h
@@ -7,7 +7,7 @@ Module Name:
 
 Abstract:
 
-    Clause and literals
+    Literals, clauses, justifications for quantifier instantiation
 
 Author:
 
@@ -49,7 +49,6 @@ namespace q {
         euf::enode* const* nodes() { return m_nodes; }
 
         euf::enode* operator[](unsigned i) const { return m_nodes[i]; }
-
     };
 
     struct clause {
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index ccf697773..fef462b70 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -328,7 +328,26 @@ namespace q {
         return l.sign ? ~ctx.mk_literal(fml) : ctx.mk_literal(fml);
     }
 
+    struct ematch::reset_in_queue : public trail<euf::solver> {
+        ematch& e;
+        reset_in_queue(ematch& e) :e(e) {}
+
+        void undo(euf::solver& ctx) override {
+            e.m_node_in_queue.reset();
+            e.m_clause_in_queue.reset();
+            e.m_in_queue_set = false;
+        }
+
+        static void insert(ematch& e) {
+            if (!e.m_in_queue_set) {
+                e.m_in_queue_set = true;
+                e.ctx.push(reset_in_queue(e));
+            }
+        }
+    };
+
     void ematch::insert_to_propagate(unsigned node_id) {
+        reset_in_queue::insert(*this);
         m_node_in_queue.assure_domain(node_id);
         if (m_node_in_queue.contains(node_id))
             return;
@@ -338,6 +357,7 @@ namespace q {
     }
 
     void ematch::insert_clause_in_queue(unsigned idx) {
+        reset_in_queue::insert(*this);
         m_clause_in_queue.assure_domain(idx);
         if (!m_clause_in_queue.contains(idx)) {
             m_clause_in_queue.insert(idx);
@@ -482,6 +502,7 @@ namespace q {
         }
         m_clause_in_queue.reset();
         m_node_in_queue.reset();
+        m_in_queue_set = true;
         if (m_inst_queue.propagate())
             propagated = true;
         return propagated;
diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h
index fa013c553..39ba72f27 100644
--- a/src/sat/smt/q_ematch.h
+++ b/src/sat/smt/q_ematch.h
@@ -53,6 +53,7 @@ namespace q {
         struct insert_binding;
         struct pop_clause;
         struct scoped_mark_reset;
+        struct reset_in_queue;
 
         
         euf::solver&                  ctx;
@@ -73,6 +74,7 @@ namespace q {
         expr_fast_mark1               m_mark;
         unsigned                      m_generation_propagation_threshold{ 3 };
         ptr_vector<app>               m_ground;
+        bool                          m_in_queue_set{ false };
         nat_set                       m_node_in_queue;
         nat_set                       m_clause_in_queue;
         unsigned                      m_qhead { 0 };