From 9bc7d5de0f25728c9fd850b6329e4091283d07ab Mon Sep 17 00:00:00 2001
From: nilsbecker <nbecker@student.ethz.ch>
Date: Sun, 29 Apr 2018 16:39:32 +0200
Subject: [PATCH] making sure equality explanations for bound terms are logged

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

diff --git a/src/smt/smt_quantifier.cpp b/src/smt/smt_quantifier.cpp
index 5d7c82415..2b134a23f 100644
--- a/src/smt/smt_quantifier.cpp
+++ b/src/smt/smt_quantifier.cpp
@@ -171,6 +171,9 @@ namespace smt {
             if (f) {
                 if (has_trace_stream()) {
                     std::ostream & out = trace_stream();
+                    for (unsigned i = 0; i < num_bindings; ++i) {
+                        log_transitive_justification(out, bindings[i]);
+                    }
                     for (auto n : used_enodes) {
                         enode *orig = std::get<0>(n);
                         enode *substituted = std::get<1>(n);