From 988e8afc2ec98013a3c83a71b55a4a943ceb99f1 Mon Sep 17 00:00:00 2001
From: nilsbecker <nilsbecker@whitecircleapps.com>
Date: Mon, 3 Dec 2018 13:50:48 +0100
Subject: [PATCH] support for logging congruence closure equality explanations
 when commutativity is used

---
 src/smt/smt_quantifier.cpp | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index f74c9d4c9..f7af9bd51 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -172,7 +172,12 @@ namespace smt {
 
                     break;
                 } else {
-                    out << "[eq-expl] #" << en->get_owner_id() << " nyi ; #" << target->get_owner_id() << "\n";
+
+                    // The e-graph only supports commutativity for binary functions
+                    out << "[eq-expl] #" << en->get_owner_id()
+                        << " cg (#" << en->get_arg(0)->get_owner_id() << " #" << target->get_arg(1)->get_owner_id()
+                        << ") (#" << en->get_arg(1)->get_owner_id() << " #" << target->get_arg(0)->get_owner_id()
+                        << ") ; #" << target->get_owner_id() << "\n";
                     break;
                 }
             case smt::eq_justification::kind::JUSTIFICATION: