From: Andrew V. Jones <andrew.jones@vector.com>
Date: Wed, 5 Aug 2020 17:38:15 +0000 (+0100)
Subject: When checking models, ensure that error message is correctly formatted (#4853)
X-Git-Tag: cvc5-1.0.0~3038
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d07c7796f75e32e46698f4f0af90a8b99577323f;p=cvc5.git

When checking models, ensure that error message is correctly formatted (#4853)

Issue
When CVC4 is checking models and encounters an issue, it presents an message like this:

Internal error detectedTHEORY_ARITH has an asserted fact that the model doesn't satisfy.
Notice: there's no space between detected and THEORY_ARITH.

Resolution
This PR ensures that the error message is correctly formatted.

Signed-off-by: Andrew V. Jones andrew.jones@vector.com
---

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index ef237e76d..a88db4494 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -2014,7 +2014,7 @@ void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
         if (val != d_true)
         {
           std::stringstream ss;
-          ss << theoryId
+          ss << " " << theoryId
              << " has an asserted fact that the model doesn't satisfy." << endl
              << "The fact: " << assertion << endl
              << "Model value: " << val << endl;