MCSAT: Preprocessor: fix equality simplification for mixed real-integer terms

SRI-CSL / yices2

The Yices SMT Solver

https://yices.csl.sri.com/

GNU General Public License v3.0

360 stars 45 forks source link

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

Closed ahmed-irfan closed 7 months ago

ahmed-irfan commented 7 months ago

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

coveralls commented 7 months ago

coverage: 65.141% (+0.001%) from 65.14% when pulling 424c00633b76dfbb599cb098b6ecee755a39bd2e on fix-mcsat-nira-eq-preprocessing into f1860fe253af1b0bd1b8bbe111c40f12134524eb on master.