DAG-disj: Fixed conjunction to disjunction in "addRestrictions"

usi-verification-and-security / golem

Solver for Constrained Horn Clauses

MIT License

34 stars 7 forks source link

DAG-disj: Fixed conjunction to disjunction in "addRestrictions" #48

Closed BritikovKI closed 11 months ago

BritikovKI commented 11 months ago

Bug Fix

Description:

The conjunction of constraints(which was used previously), restricted the paths which should not've been restricted, leading to the spurious SAFE results.

Solution:

Conjunction was replaced with disjunction, therefore as long as at least one branch is reachable from the end of TS, we still should consider the node as a potential candidate.
Two tests are added to validate this specific property.

blishko commented 11 months ago

I guess it looks good :)

Can you just specify in the PR description what was the problem and what the fix means?