Fix collect model info for higher-order (#3409)

This ensures we add lemmas when collect model info fails for the higher order extension of UF. This fixes #3405 (that benchmark now answers unknown).

1 files changed, 8 insertions, 1 deletions

diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index d3fde58a7..7a2a9ae16 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -301,12 +301,17 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
                          << std::endl;
   if (!d_te->collectModelInfo(tm))
   {
+    Trace("model-builder")
+        << "TheoryEngineModelBuilder: fail collect model info" << std::endl;
     return false;
   }
 
   // model-builder specific initialization
   if (!preProcessBuildModel(tm))
   {
+    Trace("model-builder")
+        << "TheoryEngineModelBuilder: fail preprocess build model."
+        << std::endl;
     return false;
   }
 
@@ -813,9 +818,11 @@ bool TheoryEngineModelBuilder::buildModel(Model* m)
   // modelBuilder-specific initialization
   if (!processBuildModel(tm))
   {
+    Trace("model-builder")
+        << "TheoryEngineModelBuilder: fail process build model." << std::endl;
     return false;
   }
-
+  Trace("model-builder") << "TheoryEngineModelBuilder: success" << std::endl;
   tm->d_modelBuiltSuccess = true;
   return true;
 }