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

Crash in SMT solver on input during execute request #3934

Closed ehildenb closed 3 months ago

ehildenb commented 3 months ago

Related: https://github.com/runtimeverification/k/issues/4359

I'm working on getting the last few proofs in KEVM working on the booster RPC server instead of on the legacy kprove prover, so we can remove that entry point. I came across a proof that is causing a crash in the booster due to some SMT translation error. I've attached the bug report, it should be the last request/response pair.

For context, it's from this proof: https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/examples/sum-to-n-foundry-spec.k

smt-crash.tar.gz

ehildenb commented 3 months ago

Running the same proof without the booster does not cause an SMT crash.

Additionally, running the proof without the cut-rule set there, allows it to execute past that point and pass. But I need a cut-point here for other reasons.

jberthold commented 3 months ago

~From the error message, this looks like something I investigated about 2 weeks ago: https://github.com/runtimeverification/k/issues/4400 We can implement a deduplication of the smtlib symbols in booster to address this problem (the code already exists in a commit on an open PR that I had to shelve for the time being).~ EDIT: This first looked like https://github.com/runtimeverification/k/issues/4400 but was rather an issue with how nullary functions (constants) were translated. The code to fix it (and work around the K issue) already existed on a branch, now in #3935 .