From 541b880047374f3748fbf9fa93214bae1308b1aa Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 4 Apr 2018 11:56:59 -0500 Subject: [PATCH] Do not debug check models when unknown (#1748) --- src/theory/theory_engine.cpp | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) 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); -- 2.30.2