When checking models, ensure that error message is correctly formatted (#4853)
authorAndrew V. Jones <andrew.jones@vector.com>
Wed, 5 Aug 2020 17:38:15 +0000 (18:38 +0100)
committerGitHub <noreply@github.com>
Wed, 5 Aug 2020 17:38:15 +0000 (12:38 -0500)
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
src/theory/theory_engine.cpp

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