Skip to content

Conversation

@m-carrasco
Copy link

@m-carrasco m-carrasco commented Apr 4, 2025

Hi,

This PR completes the support for boolean symbolic comparisons. The previous code did not handle cases where the two operands are symbolic.

This test case can reproduce the issue:

import tools.aqua.concolic.Verifier;

public class Main {
    public static void main(String[] args)
    {
        foo(Verifier.nondetBoolean(), Verifier.nondetBoolean());

        System.exit(0);
    }

    public static boolean foo(boolean arg1, boolean arg2)
    {
      return arg1 == arg2;
    }
}

Best regards,
Manuel

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant