Skip to content
This repository was archived by the owner on Oct 9, 2025. It is now read-only.
This repository was archived by the owner on Oct 9, 2025. It is now read-only.

"execute" endpoint returns SMT error instead of Branching result #373

@geo2a

Description

@geo2a

Consider the following scenario:

  • Proxy receives an "execute" request
  • Booster aborts and falls back to Kore
  • Kore's "execute" handler cannot decide a rule side-condition, emits a DecidePredicateUnknown warning and returns Branching
  • Proxy gets the branching result and applies the post-exec simplification to the three sub-states: the pre-branch state and two post-branch states. Now, the post-exec simplification effectively sends and internal "simplify" request to Kore. Naturally, it fails to decide the same predicate (that's Kore branched in the first place), but now it throws an DecidePredicateUnknown error
  • The error is caught by the Proxy's handler, wrapped into JsonRPC error and returned to the client.

In the end, the client gets a not-so-helpful error (which we've just made a little more helpful in #371). What the client should get instead is the Branching response, and, perhaps, the predicate that could not be decided.

I suppose the same problem is the case for all other execute results as well.

Metadata

Metadata

Assignees

Labels

No labels
No labels

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions