Skip to content

Conversation

kroening
Copy link
Collaborator

The conversion done to the RHS of an assignment differs from the downwards propagation done when adjusting the type of the operand of expressions.

This introduces a new method assignment_conversion, different from propagate_type, to implement these differences.

@kroening kroening force-pushed the assignment_conversion branch 5 times, most recently from 66de2f2 to 74dff1b Compare September 27, 2025 19:49
PR #1277 has moved the failing test case out of this file.
The conversion done to the RHS of an assignment differs from the downwards
propagation done when adjusting the type of the operand of expressions.

This introduces a new method assignment_conversion, different from
propagate_type, to implement these differences.

Three tests are changed to restore the previous circuit, as the circuit
without the downward propagation pass is too large for BDDs.
@kroening kroening force-pushed the assignment_conversion branch from 74dff1b to 18504a4 Compare September 28, 2025 08:26
@tautschnig tautschnig merged commit 10f9fc4 into main Sep 29, 2025
11 checks passed
@tautschnig tautschnig deleted the assignment_conversion branch September 29, 2025 07:52
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

Successfully merging this pull request may close these issues.

2 participants