diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-22 17:02:58 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-22 17:02:58 -0600 |
commit | fd88b18c0db55eb63d0cd0454b19810a8abee789 (patch) | |
tree | b87fed361d73f1f28b4bf8e51249e03dd7bc83b8 /src/theory/quantifiers/equality_query.cpp | |
parent | 91538b206fd5da5be289cf2d6165a854e6e5bc07 (diff) |
Fix subtyping for instantiations where internal representatives are chosen (#3641)
Diffstat (limited to 'src/theory/quantifiers/equality_query.cpp')
-rw-r--r-- | src/theory/quantifiers/equality_query.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/equality_query.cpp b/src/theory/quantifiers/equality_query.cpp index f72a0d1b4..13e7b2eb7 100644 --- a/src/theory/quantifiers/equality_query.cpp +++ b/src/theory/quantifiers/equality_query.cpp @@ -167,7 +167,9 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative(Node a, if( d_rep_score.find( r_best )==d_rep_score.end() ){ d_rep_score[ r_best ] = d_reset_count; } - Trace("internal-rep-select") << "...Choose " << r_best << " with score " << r_best_score << std::endl; + Trace("internal-rep-select") + << "...Choose " << r_best << " with score " << r_best_score + << " and type " << r_best.getType() << std::endl; Assert(r_best.getType().isSubtypeOf(v_tn)); v_int_rep[r] = r_best; if( r_best!=a ){ |