search

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework
BSD 3-Clause "New" or "Revised" License
208 stars 41 forks source link

Simplify the remainder predicate before checking its satisfiability #3949

Closed geo2a closed 1 month ago

geo2a commented 3 months ago

Needs https://github.com/runtimeverification/haskell-backend/pull/3943

This is a more radical variant of https://github.com/runtimeverification/haskell-backend/pull/3943 that simplifies the remainder before checking it for satisfiability. If the remainder is satisfiable, we do not simplify it again in applyRemainder.

geo2a commented 1 month ago

This PR is stale and will anyway be eventually subsumed by https://github.com/runtimeverification/haskell-backend/pull/3960