runtimeverification / pyk

Python tools for the K Framework
BSD 3-Clause "New" or "Revised" License
13 stars 2 forks source link

Allowing multiple constraints in splits preceding nodes to be refuted #1066

Closed PetarMax closed 5 months ago

PetarMax commented 5 months ago

Currently, the refutation mechanism cannot handle the case in which the split preceding the node to be refuted contains more than one constraint. Such scenarios, however, have become commonplace given the newly introduced KCFG minimization mechanism.

This PR extends the refutation mechanism by allowing it to handle splits with multiple constraints.