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

Haskell backend crashed on proof with uninformative error #2565

Closed ehildenb closed 3 years ago

ehildenb commented 3 years ago

K version: 5.0.24 Kore version:

Kore version 0.43.0.0
Git:
  revision:     4f32a3b7c80d33e1e8cf81f8cbbef566ba378df7
  branch:       HEAD
  last commit:  Fri Apr 16 09:49:29 2021 -0600

This example comes from https://github.com/makerdao/mkr-mcd-spec.

The unhelpful output is:

kore-exec: [5035258] Error (ErrorException):
    Assertion failed
    CallStack (from HasCallStack):
      assert, called at src/Kore/Equation/Application.hs:200:27 in kore-0.43.0.0-HgLSPgFtvBzHoiXRxMegel:Kore.Equation.Application
      attemptEquation, called at src/Kore/Step/Axiom/EvaluationStrategy.hs:148:13 in kore-0.43.0.0-HgLSPgFtvBzHoiXRxMegel:Kore.Step.Axiom.EvaluationStrategy
    Please file a bug report: https://github.com/kframework/kore/issues
Created bug report: kore-exec.tar.gz
[Error] Critical: Haskell Backend execution failed with code 1 and produced no
output.

I've attached the generated kore-exec.tar.gz.

ana-pantilie commented 3 years ago

This looks like the same issue as https://github.com/kframework/kore/issues/2523.

ttuegel commented 3 years ago

This is exactly the same as #2523.

The error is exactly as helpful as it is supposed to be, because it led you to file this bug report. There is no intervention that the user could do to avoid this error.