diff options
Diffstat (limited to 'src/theory/quantifiers/rewrite_engine.cpp')
-rw-r--r-- | src/theory/quantifiers/rewrite_engine.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/theory/quantifiers/rewrite_engine.cpp b/src/theory/quantifiers/rewrite_engine.cpp index 05e33c7b2..a70d36ac0 100644 --- a/src/theory/quantifiers/rewrite_engine.cpp +++ b/src/theory/quantifiers/rewrite_engine.cpp @@ -38,7 +38,6 @@ struct PrioritySort { RewriteEngine::RewriteEngine( context::Context* c, QuantifiersEngine* qe ) : QuantifiersModule(qe) { - d_true = NodeManager::currentNM()->mkConst( true ); d_needsSort = false; } @@ -277,7 +276,7 @@ void RewriteEngine::registerQuantifier( Node f ) { body_c.push_back( d_rr[f][1][j].negate() ); } } - }else if( d_rr[f][1]!=d_true ){ + }else if( d_rr[f][1]!=d_quantEngine->getTermDatabase()->d_true ){ if( MatchGen::isHandled( d_rr[f][1] ) ){ body_c.push_back( d_rr[f][1].negate() ); } @@ -307,4 +306,4 @@ Node RewriteEngine::getInstConstNode( Node n, Node q ) { }else{ return it->second; } -}
\ No newline at end of file +} |