Make handling of illegal internal representatives in quantifiers engine more robust (#4034)

Fixes #4002 (that benchmark is now unknown).

The experimental option --cbqi-all previously had some issues when combined with finite model finding. When these two options are used simultaneously, it may be the case that certain equivalence classes are "illegal" since they contain only terms that are ineligible for instantiation.

The previous code threw a warning when this occurred which in extreme cases allowed for potentially ineligible terms for instantiation. The new code is more conservative: we never choose illegal internal representatives and instead set the incomplete flag in finite model finding when this occurs.

A block of code changed indentation in this PR, which was updated to the new standards.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp
index 4012f687f..3fff374a7 100644
--- a/src/theory/quantifiers/fmf/model_engine.cpp
+++ b/src/theory/quantifiers/fmf/model_engine.cpp
@@ -182,6 +182,11 @@ int ModelEngine::checkModel(){
       Trace("model-engine-debug") << "   Term reps : ";
       for( size_t i=0; i<it->second.size(); i++ ){
         Node r = d_quantEngine->getInternalRepresentative( it->second[i], Node::null(), 0 );
+        if (r.isNull())
+        {
+          // there was an invalid equivalence class
+          d_incomplete_check = true;
+        }
         Trace("model-engine-debug") << r << " ";
       }
       Trace("model-engine-debug") << std::endl;