search

usi-verification-and-security / opensmt

The opensmt solver
Other
78 stars 18 forks source link

[WIP] Checking in `mkConst` that every `Number` of sort Int is indeed integer #813

Open Tomaqa opened 6 days ago

Tomaqa commented 6 days ago

This assertion fails with substitutions and also in FarkasInterpolator::getFlexibleInterpolant in TEST_F(LIAInterpolationTest, test_InterpolationLRASat). We should probably forbid such substitutions. In the interpolation, I am not sure if the test makes sense or if the situation must be handled more properly.