This PR introduces fixes for two problems.
One is a corner case in model-based projection where a presence of ~false literal would cause incorrect computation of extended model when handling divisibility constraints.
After this fix, proof production on the same example showed that after the recent changes in the normalization process we no longer version auxiliary variables introduced during elimination of ITE/DIV/MOD operators.
The proposed change here is to version those variables immediately after their creation.
This PR introduces fixes for two problems. One is a corner case in model-based projection where a presence of ~false literal would cause incorrect computation of extended model when handling divisibility constraints.
After this fix, proof production on the same example showed that after the recent changes in the normalization process we no longer version auxiliary variables introduced during elimination of ITE/DIV/MOD operators. The proposed change here is to version those variables immediately after their creation.