Do not debug check models when unknown (#1748)

1 files changed, 6 insertions, 1 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 375027d34..f3489f5ad 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -639,7 +639,12 @@ void TheoryEngine::check(Theory::Effort effort) {
         AlwaysAssert(d_curr_model->isBuiltSuccess());
         if (options::produceModels())
         {
-          d_curr_model_builder->debugCheckModel(d_curr_model);
+          // if we are incomplete, there is no guarantee on the model.
+          // thus, we do not check the model here. (related to #1693)
+          if (!d_incomplete)
+          {
+            d_curr_model_builder->debugCheckModel(d_curr_model);
+          }
           // Do post-processing of model from the theories (used for THEORY_SEP
           // to construct heap model)
           postProcessModel(d_curr_model);