SRI-CSL / yices2 / 7052784624

66%

push

github

MCSAT: Preprocessor: fix equality simplification for mixed real-integer terms (#481)

It is wrong to remove integer variable by substituting a real variable.
This was happening in the mcsat preprocessor during equality propagation of the top-level equality x_int_var = y_real_var.
This PR fixes this issue by not doing propagation of such equalities.

This PR:

Fixes mcsat preprocessor
Adds regression tests
Adds api test

* don't propagate top-level equality if the types of lhs and rhs are not the same

* add regression tests

* api test

* fix corner case of ARITH_EQ_TERM in detecting is_mixed

* update test

3 of 3 new or added lines in 1 file covered. (100.0%)

79302 of 121739 relevant lines covered (65.14%)

1507543.78 hits per line