diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-05-08 16:28:22 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-05-08 16:28:22 -0500 |
commit | cfaa03f3db71dc2805b695f98b073431d0430e43 (patch) | |
tree | 29a005932e186354f2966603601982ca8448c89f /src/theory/theory_engine.cpp | |
parent | f5e3739358b98d9a6ebc16fbc5aed9edee1483dc (diff) |
Infrastructure for approximations in model output (#1884)
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r-- | src/theory/theory_engine.cpp | 4 |
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); } |