added option --model-u-dt-enum for outputting uninterpreted sorts as datatype enumerations + minor update to array rewriter to improve output for this option, minor refactoring of representative selection for quantifier instantiation, initial draft of disequality propagation option --uf-ss-deq-prop, other refactoring of uf strong solver, fixed bug 496, improvement for fmf enumeration of finite built-in sorts

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 ){