Infrastructure for approximations in model output (#1884)

1 files changed, 3 insertions, 1 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index edea22fbf..11da42e07 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -645,7 +645,9 @@ void TheoryEngine::check(Theory::Effort effort) {
         {
           // 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)
+          // we also don't debug-check the model if the checkModels()
+          // is not enabled.
+          if (!d_incomplete && options::checkModels())
           {
             d_curr_model_builder->debugCheckModel(d_curr_model);
           }