Skip to content

Interpol mod fix - #900

Open
BritikovKI wants to merge 9 commits into
masterfrom
interpol_mod_fix
Open

Interpol mod fix#900
BritikovKI wants to merge 9 commits into
masterfrom
interpol_mod_fix

Conversation

@BritikovKI

@BritikovKI BritikovKI commented Jul 22, 2026

Copy link
Copy Markdown
Member

This pull request is supposed to fix issue #893

@BritikovKI
BritikovKI marked this pull request as draft July 22, 2026 13:28
@BritikovKI
BritikovKI marked this pull request as ready for review August 11, 2026 15:25
@BritikovKI

Copy link
Copy Markdown
Member Author

This pull request parses the produced interpolant (Linear Integer Arithmetic particularly) and replaces introduced div/mod variables with exact div/mod representations

@BritikovKI
BritikovKI requested review from Tomaqa and blishko August 11, 2026 15:48
@Tomaqa

Tomaqa commented Aug 12, 2026

Copy link
Copy Markdown
Member

Could you add a unit/regression test such as the one in #893? Ideally, it should fail before the fix and pass after.

@BritikovKI

Copy link
Copy Markdown
Member Author

Could you add a unit/regression test such as the one in #893? Ideally, it should fail before the fix and pass after.

Oh, sorry, my bad, I had a commit locally but forgot to push it...

@Tomaqa

Tomaqa commented Aug 14, 2026

Copy link
Copy Markdown
Member

The test does not fail before the fix. I also tried the Debug mode, but I assume the test is not supposed to only trigger or not trigger a debug assertion failure.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants