summaryrefslogtreecommitdiff
path: root/src/theory/inst_match.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/inst_match.cpp')
-rw-r--r--src/theory/inst_match.cpp3
1 files changed, 0 insertions, 3 deletions
diff --git a/src/theory/inst_match.cpp b/src/theory/inst_match.cpp
index c90483fa3..bad7e34cb 100644
--- a/src/theory/inst_match.cpp
+++ b/src/theory/inst_match.cpp
@@ -272,9 +272,6 @@ void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){
Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;
- //get the equality engine
- Theory* th_uf = qe->getTheoryEngine()->getTheory( theory::THEORY_UF );
- uf::InstantiatorTheoryUf* ith = (uf::InstantiatorTheoryUf*)th_uf->getInstantiator();
//create candidate generator
if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback