projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: ce2fa6a) | patch
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)
commitd07c7796f75e32e46698f4f0af90a8b99577323f
treeaa7101a21cb4f5305f4dfb974022b100bf23b7c6tree
parentce2fa6ad8858c70aebf253b910bea3726065e85dcommit | 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
src/theory/theory_engine.cpp diff | blob | history