CogniCrypt version: 4.2.1

From what I understand the error messages should be formed as:

"Constraint ""
+ evaluableConstraint
+ "" on object "
+ getSeed().getFact().getVariableName()
+ " is violated due to the following reason: "
+ violatedConstraint.getErrorMessage()

However, the last part does not appear to work for constraints that include implications or comparisons. Here the message cuts off after "due to the following reason: "

Some examples (the first three occur for the file CryptoAnalysisTargets/CryptoMisuseExamples/src/main/java/main/Msg.java in this repo, the rest are from my own tests):

• Constraint "transformation in {AES} => transformation in {GCM, CTR, CTS, CFB, OFB}" on object r0 is violated due to the following reason:

• Constraint "noCallTo[init(int, java.security.cert.Certificate), init(int, java.security.cert.Certificate, java.security.SecureRandom), init(int, java.security.Key), init(int, java.security.Key, java.security.SecureRandom), init(int, java.security.Key, java.security.spec.AlgorithmParameterSpec), init(int, java.security.Key, java.security.AlgorithmParameters), init(int, java.security.Key, java.security.spec.AlgorithmParameterSpec, java.security.SecureRandom), init(int, java.security.Key, java.security.AlgorithmParameters, java.security.SecureRandom)] => transformation in {AES, RSA, PBEWithHmacSHA224AndAES_128, PBEWithHmacSHA256AndAES_128, PBEWithHmacSHA384AndAES_128, PBEWithHmacSHA512AndAES_128, PBEWithHmacSHA224AndAES_256, PBEWithHmacSHA256AndAES_256, PBEWithHmacSHA384AndAES_256, PBEWithHmacSHA512AndAES_256}" on object $r4 is violated due to the following reason:

• Constraint "algorithm in {RSA} => keysize in {4096, 3072}" on object r0 is violated due to the following reason:

• Constraint "length[prePlainText] >= prePlainTextOffset + prePlainTextLen" on object r0 is violated due to the following reason:

• Constraint "prePlainTextLen > 0" on object r0 is violated due to the following reason:

• Constraint "transformation in {CTR, CTS, CFB, OFB} && encmode == 1 => callTo[getIV()]" on object r0 is violated due to the following reason: