usi-verification-and-security / opensmt

The opensmt solver
Other
78 stars 18 forks source link

FastRational: Eliminate potential UB #663

Closed blishko closed 10 months ago

blishko commented 10 months ago

Casting away const and then modifying the object is UB if the original object was const. From cppreference: "Modifying a const object through a non-const access path results in undefined behavior."

We fix the problem by making mpq and state mutable, as we can change the inner representaton in certain circumstances without changing the rational value represented by the object.

Fixes #662.