From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Wed, 4 Apr 2018 16:56:59 +0000 (-0500)
Subject: Do not debug check models when unknown (#1748)
X-Git-Tag: cvc5-1.0.0~5180
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=541b880047374f3748fbf9fa93214bae1308b1aa;p=cvc5.git

Do not debug check models when unknown (#1748)
---

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