From d07c7796f75e32e46698f4f0af90a8b99577323f Mon Sep 17 00:00:00 2001 From: "Andrew V. Jones" Date: Wed, 5 Aug 2020 18:38:15 +0100 Subject: [PATCH] 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 --- src/theory/theory_engine.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; -- 2.30.2