From e955bd09e52d3277555af3e2f8a0933bfaa2f36a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 9 Nov 2020 13:08:46 -0800
Subject: [PATCH] push equality for #4740

https://github.com/Z3Prover/z3/issues/4740#issuecomment-711460353
---
 src/smt/smt_internalizer.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 1caaa4663..28fdaf3b5 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -982,6 +982,7 @@ namespace smt {
                 bool_var v = enode2bool_var(e);
                 assign(literal(v), mk_justification(eq_propagation_justification(e->get_arg(0), e->get_arg(1))));
                 e->m_cg    = e;
+                push_eq(e, m_true_enode, eq_justification());
             }
             else {
                 if (cgc_enabled) {