Skip to content

Conversation

@Stevengre
Copy link
Contributor

No description provided.

@Stevengre Stevengre marked this pull request as draft October 24, 2025 03:00
@Stevengre Stevengre marked this pull request as ready for review October 24, 2025 06:21
@Stevengre
Copy link
Contributor Author

Stevengre commented Oct 24, 2025

@jberthold I failed to pass test_prove_rs[interior-mut-fail]. I think it might be caused by preserve-definedness missing problem, but I'm not sure. Do you have any idea about this error?

====================================================== short test summary info ======================================================
FAILED kmir/src/tests/integration/test_integration.py::test_prove_rs[interior-mut-fail] - pyk.cterm.symbolic.CTermSMTError: #Ceil ( ListItem ( newLocal ( ty ( 68 ) , mutabilityMut ) ) ListItem ( typedValue ( Integer ( ...
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! stopping after 1 failures !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! xdist.dsession.Interrupted: stopping after 1 failures !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
====================================== 1 failed, 198 passed, 40 skipped in 2194.85s (0:36:34) =======================================

Yes, the #Ceil indicates that the legacy backend did a rewrite here, possibly because you are missing a preserves-definedness. Taking a closer look

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We have a make target update-smir-json which you could use. You just have to create an empty my/new/file.smir.json file first and then run make update-smir-json TARGETS=my/new/file.smir.json

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thank you! Could I keep this file or just delete it?

Copy link
Member

@jberthold jberthold left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Looking good now, and the examples are working!
I have two suggestions for refactoring (to let fewer exceptional cases pass through) but pre-approving.

@automergerpr-permission-manager automergerpr-permission-manager bot merged commit c8d9260 into master Oct 27, 2025
7 checks passed
@automergerpr-permission-manager automergerpr-permission-manager bot deleted the jh/decode-struct branch October 27, 2025 07:01
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants