Merge branch 'master' into mkExceptionPublicmkExceptionPublic

4 files changed, 22 insertions, 17 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);
diff --git a/test/regress/regress0/cores/issue4971-0.smt2 b/test/regress/regress0/cores/issue4971-0.smt2
index 75878183c..16fdc2b77 100644
--- a/test/regress/regress0/cores/issue4971-0.smt2
+++ b/test/regress/regress0/cores/issue4971-0.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --incremental -q --check-unsat-cores
-; EXPECT: unknown
+; COMMAND-LINE: --incremental -q --check-unsat-cores --cegqi-full
+; EXPECT: unsat
 ; EXPECT: unsat
 ; EXPECT: (
 ; EXPECT: IP_1
@@ -15,4 +15,4 @@
 (assert (! (or (< (abs 404) i4) v14 v1) :named IP_51))
 (check-sat)
 (check-sat-assuming (IP_33 IP_51))
-(get-unsat-core)
\ No newline at end of file
+(get-unsat-core)
diff --git a/test/regress/regress0/cores/issue4971-1.smt2 b/test/regress/regress0/cores/issue4971-1.smt2
index 9bb4f3e84..2ac70735c 100644
--- a/test/regress/regress0/cores/issue4971-1.smt2
+++ b/test/regress/regress0/cores/issue4971-1.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --incremental -q --check-unsat-cores
 ; COMMAND-LINE: --incremental -q --check-unsat-cores --unsat-cores-mode=sat-proof
 ; EXPECT: sat
 ; EXPECT: sat