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 ef237e76daefea2ba5f07ec67009bf5fc7395862..a88db44948983b7806f40e19f7d799297460178b 100644 (file)
--- 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;