mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

making sure equality explanations for bound terms are logged

Browse source
This commit is contained in:
nilsbecker 2018-04-29 16:39:32 +02:00
parent 7a03f19456
commit 9bc7d5de0f
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_quantifier.cpp
View file

@ -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);