diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-23 16:59:48 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-23 16:59:48 -0500 |
commit | aa3b60104a0026c078eea1d19506e8bf4c3d9763 (patch) | |
tree | 7dd9d34248d533918c304965131b11dcef6cf2b6 /src/theory/quantifiers/candidate_generator.cpp | |
parent | 2deb3a617f068af25457db23eae326dae2bf2ae2 (diff) |
Fix bug in E-matching Real/Int terms.
Diffstat (limited to 'src/theory/quantifiers/candidate_generator.cpp')
-rw-r--r-- | src/theory/quantifiers/candidate_generator.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 9b5e506ea..799513171 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -175,7 +175,7 @@ Node CandidateGeneratorQELitEq::getNextCandidate(){ while( !d_eq.isFinished() ){ Node n = (*d_eq); ++d_eq; - if( n.getType()==d_match_pattern[0].getType() ){ + if( n.getType().isSubtypeOf( d_match_pattern[0].getType() ) ){ //an equivalence class with the same type as the pattern, return reflexive equality return NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), n, n ); } @@ -228,7 +228,7 @@ Node CandidateGeneratorQEAll::getNextCandidate() { while( !d_eq.isFinished() ){ Node n = (*d_eq); ++d_eq; - if( n.getType()==d_match_pattern.getType() ){ + if( n.getType().isSubtypeOf( d_match_pattern.getType() ) ){ //an equivalence class with the same type as the pattern, return it return n; } |