Do not allow duplication of function definitions. Set incomplete flag in model builder.

1 files changed, 4 insertions, 0 deletions

diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index eede5c3a8..6ec347031 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -96,6 +96,10 @@ void ModelEngine::check( Theory::Effort e, unsigned quant_e ){
       //CVC4 will answer SAT or unknown
       Trace("fmf-consistent") << std::endl;
       debugPrint("fmf-consistent");
+      //if the check was incomplete, we must set incomplete flag
+      if( d_incomplete_check ){
+        d_quantEngine->getOutputChannel().setIncomplete();
+      }
     }else{
       //otherwise, the search will continue
     }