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.

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 6ac5b0289e50123524b57d481bacfd392f7ecb84..08e6f317c6898e8c4fac1a859f5a8f9b63717c9a 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -80,9 +80,16 @@ 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"

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 8236486dd55a6da73a176e0232d68aa3ed72028e..899da4d4a5e88d87edbe258246aed760cd7b4af7 100644 (file)
--- 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 d4e83c672b4feb83097c2112c9044e2bd6a264f6..3c0a2cd8ff7ecdda8cc7133b891764069de84cbe 100644 (file)
--- 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 68ad25490cc07f9b5eca6847e7c4aed3779ca866..e829c1db4f5608e859483ff9534f96360d18e535 100644 (file)
--- 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 78b4db656ec5290e6d5aac295f39717ea4a23e0e..83b9a872e952a41df37403235636fa19d9966c94 100755 (executable)
--- 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 \