diff options
| author | Andrew V. Jones <andrew.jones@vector.com> | 2020-08-05 18:38:15 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-05 12:38:15 -0500 |
| commit | d07c7796f75e32e46698f4f0af90a8b99577323f (patch) | |
| tree | aa7101a21cb4f5305f4dfb974022b100bf23b7c6 | |
| parent | ce2fa6ad8858c70aebf253b910bea3726065e85d (diff) | |
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
| -rw-r--r-- | src/theory/theory_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
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; |