usi-verification-and-security / opensmt

The opensmt solver
Other
77 stars 18 forks source link

Extended test_LRALogicMkTerms:ConstantSimplification of 1/3 #748

Closed Tomaqa closed 2 months ago

Tomaqa commented 2 months ago

Added additional test that checks the case of creating "1/3" instead of just "1/2". This can catch errors if the implementation of rationals is changed since 1/3 does not have finite representation if the numerator and denominator are not separated (such as with floats).