From b71bf740b517c3a530d92c33bd24769330708d76 Mon Sep 17 00:00:00 2001
From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 12 Jul 2021 12:20:57 -0500
Subject: [PATCH] Improvements to debug check model (#6861)

This makes it so that debug-check-models applies in production mode, not just in debug mode. It also verifies that type constraints are met.
---
 src/theory/model_manager.cpp        |  6 +++---
 src/theory/theory_model_builder.cpp | 26 +++++++++++++++-----------
 2 files changed, 18 insertions(+), 14 deletions(-)

diff --git a/src/theory/model_manager.cpp b/src/theory/model_manager.cpp
index c1c488f65..0d56dd6db 100644
--- a/src/theory/model_manager.cpp
+++ b/src/theory/model_manager.cpp
@@ -95,10 +95,10 @@ bool ModelManager::buildModel()
   // now, finish building the model
   d_modelBuiltSuccess = finishBuildModel();
 
-  if (Trace.isOn("model-builder"))
+  if (Trace.isOn("model-final"))
   {
-    Trace("model-builder") << "Final model:" << std::endl;
-    Trace("model-builder") << d_model->debugPrintModelEqc() << std::endl;
+    Trace("model-final") << "Final model:" << std::endl;
+    Trace("model-final") << d_model->debugPrintModelEqc() << std::endl;
   }
 
   Trace("model-builder") << "ModelManager: model built success is "
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp
index e3e197953..e43cb26c8 100644
--- a/src/theory/theory_model_builder.cpp
+++ b/src/theory/theory_model_builder.cpp
@@ -1089,7 +1089,6 @@ void TheoryEngineModelBuilder::postProcessModel(bool incomplete, TheoryModel* m)
 
 void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm)
 {
-#ifdef CVC5_ASSERTIONS
   if (tm->hasApproximations())
   {
     // models with approximations may fail the assertions below
@@ -1111,7 +1110,7 @@ void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm)
       // if Boolean, it does not necessarily have a constant representative, use
       // get value instead
       rep = tm->getValue(eqc);
-      Assert(rep.isConst());
+      AlwaysAssert(rep.isConst());
     }
     eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
     for (; !eqc_i.isFinished(); ++eqc_i)
@@ -1119,21 +1118,26 @@ void TheoryEngineModelBuilder::debugCheckModel(TheoryModel* tm)
       Node n = *eqc_i;
       static int repCheckInstance = 0;
       ++repCheckInstance;
-
+      AlwaysAssert(rep.getType().isSubtypeOf(n.getType()))
+          << "Representative " << rep << " of " << n
+          << " violates type constraints (" << rep.getType() << " and "
+          << n.getType() << ")";
       // non-linear mult is not necessarily accurate wrt getValue
       if (n.getKind() != kind::NONLINEAR_MULT)
       {
-        Debug("check-model::rep-checking") << "( " << repCheckInstance << ") "
-                                           << "n: " << n << endl
-                                           << "getValue(n): " << tm->getValue(n)
-                                           << endl
-                                           << "rep: " << rep << endl;
-        Assert(tm->getValue(*eqc_i) == rep)
-            << "run with -d check-model::rep-checking for details";
+        if (tm->getValue(*eqc_i) != rep)
+        {
+          std::stringstream err;
+          err << "Failed representative check:" << std::endl
+              << "( " << repCheckInstance << ") "
+              << "n: " << n << endl
+              << "getValue(n): " << tm->getValue(n) << std::endl
+              << "rep: " << rep << std::endl;
+          AlwaysAssert(tm->getValue(*eqc_i) == rep) << err.str();
+        }
       }
     }
   }
-#endif /* CVC5_ASSERTIONS */
 
   // builder-specific debugging
   debugModel(tm);
-- 
2.30.2