Use debug-check-model to enable internal debugging in check-model (#4480)

Notice this also updates our regression script to use --debug-check-model, preserving previous behavior.

Fixes #4461, fixes #4470, fixes #4471, fixes #4475, fixes #4448, fixes #4466, fixes #4460, fixes #4458, fixes #4455, fixes #4456, fixes #4386, fixes #4385, fixes #4478, fixes #4474.

5 files changed, 22 insertions, 6 deletions

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 6ac5b0289..08e6f317c 100644
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -80,10 +80,17 @@ header = "options/smt_options.h"
   long       = "check-models"
   type       = "bool"
   notifies   = ["notifyBeforeSearch"]
-  read_only  = true
   help       = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions"
 
 [[option]]
+  name       = "debugCheckModels"
+  category   = "regular"
+  long       = "debug-check-models"
+  type       = "bool"
+  notifies   = ["notifyBeforeSearch"]
+  help       = "after SAT/INVALID/UNKNOWN, check that the generated model satisfies user and internal assertions"
+
+[[option]]
   name       = "dumpModels"
   category   = "regular"
   long       = "dump-models"
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 8236486dd..899da4d4a 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -46,6 +46,11 @@ namespace smt {
 void setDefaults(SmtEngine& smte, LogicInfo& logic)
 {
   // implied options
+  if (options::debugCheckModels())
+  {
+    Notice() << "SmtEngine: setting checkModel" << std::endl;
+    options::checkModels.set(true);
+  }
   if (options::checkModels() || options::dumpModels())
   {
     Notice() << "SmtEngine: setting produceModels" << std::endl;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index d4e83c672..3c0a2cd8f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2514,8 +2514,11 @@ void SmtEngine::checkModel(bool hardFailure) {
   }
 
   // Check individual theory assertions
-  d_theoryEngine->checkTheoryAssertionsWithModel(hardFailure);
-
+  if (options::debugCheckModels())
+  {
+    d_theoryEngine->checkTheoryAssertionsWithModel(hardFailure);
+  }
+  
   // Output the model
   Notice() << *m;
 
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index 68ad25490..e829c1db4 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -1115,7 +1115,7 @@ void TheoryEngineModelBuilder::postProcessModel(bool incomplete, Model* m)
   TheoryModel* tm = static_cast<TheoryModel*>(m);
   Assert(tm != nullptr);
   // debug-check the model if the checkModels() is enabled.
-  if (options::checkModels())
+  if (options::debugCheckModels())
   {
     debugCheckModel(tm);
   }
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 78b4db656..83b9a872e 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -343,9 +343,10 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper,
             '--check-synth-sol' not in all_args:
             extra_command_line_args = ['--check-synth-sol']
         if re.search(r'^(sat|invalid|unknown)$', expected_output) and \
+           '--no-debug-check-models' not in all_args and \
            '--no-check-models' not in all_args and \
-           '--check-models' not in all_args:
-            extra_command_line_args = ['--check-models']
+           '--debug-check-models' not in all_args:
+            extra_command_line_args = ['--debug-check-models']
         if proofs and re.search(r'^(unsat|valid)$', expected_output):
             if '--no-check-proofs' not in all_args and \
                '--check-proofs' not in all_args and \