Skip to content

Conversation

@rcosta358
Copy link
Collaborator

@rcosta358 rcosta358 commented Nov 12, 2025

There was a bug in the expression simplification logic where an expression, e.g., x == 1 was being simplified to true, since the variable x was replaced with its known value 1, resulting in the tautology 1 == 1 which would then get folded to true.

This would then result in error messages such as "true is not a subtype of #x_0 < 0".

This was fixed in the VariableResolver by checking if the expression we want to extract the variables from is a single top-level equality and, in this case, don't add x -> 1 to the variable map.

Also added some tests for the VariableResolver and an extra test case for this case in the ExpressionSimplifierTest.

@rcosta358 rcosta358 self-assigned this Nov 12, 2025
@rcosta358 rcosta358 added the bug Something isn't working label Nov 12, 2025
@rcosta358 rcosta358 changed the title Fix Single Equality Expression Simplification Fix Single Equality Simplification Nov 13, 2025
Copy link
Collaborator

@CatarinaGamboa CatarinaGamboa left a comment

Choose a reason for hiding this comment

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

lgtm

@rcosta358 rcosta358 merged commit 01a39ff into main Nov 13, 2025
1 check passed
@rcosta358 rcosta358 deleted the fix-single-eq-simplification branch November 15, 2025 19:09
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug Something isn't working

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants