Open Stevengre opened 2 weeks ago
Thanks for reporting this issue.
Let's simplify the example. You can
CTerm
directly, i.e. CTerm(KApply(...), ...)
;CTerm
, i.e. reduce the number of sub-terms so that the issue is still reproducible.Also, please push a branch with the test so that the issue is easy to reproduce.
Thanks for your suggestion. I’ve already constructed a test in this branch: https://github.com/runtimeverification/k/tree/4496-ctermmatch_with_constraint-does-not-return-expected-csubstconstraints. I hope this can help.
I opened a PR with your test to start the discussion (does not yet fix the issue):
The fix should be straightforward, we just need to figure out what the intended semantics for CTerm.constraint
is. For that, all uses need to be inspected.
Hi @tothtamas28 !
I am encountering an issue with
CTerm.match_with_constraint
where it does not provide the expectedCSubst
that can be used to transformself
intoother
viaCSubst.apply
. Instead, I am receiving an empty constraint. I suspect there may be an issue with the_ml_impl
method.Here is my test harness:
Could you please help me identify what might be going wrong?
Thank you!