Investigate the background of #3917 (injections and SMT)

runtimeverification / haskell-backend

The symbolic execution engine powering the K Framework

BSD 3-Clause "New" or "Revised" License

204 stars 39 forks source link

Investigate the background of #3917 (injections and SMT) #3920

Open jberthold opened 3 weeks ago

jberthold commented 3 weeks ago

After fixing the immediate problem reported in #3917, we should minimise the definition and integration test to understand better how this injection caused an SMT translation problem that was previously not observed.

Also, the integration test should be run against kore-rpc, too.