From 30c9cda61e49c13e602daf2ecc40c73496ca4f14 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 1 Dec 2022 10:04:33 +0900
Subject: [PATCH] increment generation for literals created during E-matching

---
 src/sat/smt/q_ematch.cpp | 5 +++--
 src/sat/smt/q_ematch.h   | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 9335c576b..573003305 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -383,7 +383,7 @@ namespace q {
         sat::literal_vector lits;
         lits.push_back(~j.m_clause.m_literal);
         for (unsigned i = 0; i < j.m_clause.size(); ++i) 
-            lits.push_back(instantiate(j.m_clause, j.m_binding, j.m_clause[i])); 
+            lits.push_back(instantiate(j.m_clause, j.m_generation, j.m_binding, j.m_clause[i])); 
         m_qs.log_instantiation(lits, &j);
         euf::th_proof_hint* ph = nullptr;
         if (ctx.use_drat()) 
@@ -418,11 +418,12 @@ namespace q {
         m_qs.log_instantiation(~c.m_literal, lit);
     }
 
-    sat::literal ematch::instantiate(clause& c, euf::enode* const* binding, lit const& l) {
+    sat::literal ematch::instantiate(clause& c, unsigned generation, euf::enode* const* binding, lit const& l) {
         expr_ref_vector _binding(m);
         for (unsigned i = 0; i < c.num_decls(); ++i)
             _binding.push_back(binding[i]->get_expr());
         var_subst subst(m);
+        euf::solver::scoped_generation sg(ctx, generation + 1);
         auto sub = [&](expr* e) {
             expr_ref r = subst(e, _binding);
             //ctx.rewrite(r);
diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h
index c04107b3b..cbeb34679 100644
--- a/src/sat/smt/q_ematch.h
+++ b/src/sat/smt/q_ematch.h
@@ -103,7 +103,7 @@ namespace q {
         void ensure_ground_enodes(clause const& c);
 
         void instantiate(binding& b);
-        sat::literal instantiate(clause& c, euf::enode* const* binding, lit const& l);
+        sat::literal instantiate(clause& c, unsigned generation, euf::enode* const* binding, lit const& l);
 
         // register as callback into egraph.
         void on_merge(euf::enode* root, euf::enode* other);