diff options
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index 53977ee4f..75cc10615 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -84,16 +84,18 @@ bool InstantiationEngine::doInstantiationRound( Theory::Effort effort ){ //add cbqi lemma //get the counterexample literal Node ceLit = d_quantEngine->getTermDatabase()->getCounterexampleLiteral( f ); - //require any decision on cel to be phase=true - d_quantEngine->getOutputChannel().requirePhase( ceLit, true ); - Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; - //add counterexample lemma - NodeBuilder<> nb(kind::OR); - nb << f << ceLit; - Node lem = nb; - Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma( lem ); - addedLemma = true; + if( !ceLit.isNull() ){ + //require any decision on cel to be phase=true + d_quantEngine->getOutputChannel().requirePhase( ceLit, true ); + Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl; + //add counterexample lemma + NodeBuilder<> nb(kind::OR); + nb << f << ceLit; + Node lem = nb; + Debug("cbqi-debug") << "Counterexample lemma : " << lem << std::endl; + d_quantEngine->getOutputChannel().lemma( lem ); + addedLemma = true; + } } } if( addedLemma ){ |