Skip to content

Possible improvements to PDKIND engine #122

@blishko

Description

@blishko

Seems like PDKIND could benefit from improvements in reachability checks:

  • Try using solver incrementally in reachability frames (at least the transition relation could be inserted only once)
  • Try something akin to must-summaries in Spacer

Benchmark to test: LRA-TS/chc-LRA-TS_048.smt2

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions