Skip to content

PRED_SPLIT produces false negative results for XCFA #267

@leventeBajczi

Description

@leventeBajczi
Contributor

There are wrong results with the current version (5.1.1) of Theta.
See results:
split.zip
Ignore floats-cbmc-regression/float8.yml in the results, that has a different root cause.

Activity

leventeBajczi

leventeBajczi commented on Jun 15, 2024

@leventeBajczi
ContributorAuthor

Until this is fixed, the frontend rejects the --domain PRED_SPLIT argument with the message

Validation failed for rule NoPredSplitUntilFixed(https://github.com/ftsrg/theta/issues/267).

leventeBajczi

leventeBajczi commented on Jun 17, 2024

@leventeBajczi
ContributorAuthor

It seems like this issue exists only with lazy pruning.

added
xcfaIssue is XCFA specific (not core or XSTS or other formalisms)
on Nov 14, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

Labels

xcfaIssue is XCFA specific (not core or XSTS or other formalisms)

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

    Development

    No branches or pull requests

      Participants

      @AdamZsofi@leventeBajczi@szdan97

      Issue actions

        PRED_SPLIT produces false negative results for XCFA · Issue #267 · ftsrg/theta