goblint / analyzer

Static analysis framework for C
https://goblint.in.tum.de
MIT License
160 stars 72 forks source link

make cil_exp_of_linexpr1 work with fractional expressions #1493

Closed DrMichaelPetter closed 23 hours ago

DrMichaelPetter commented 1 month ago

Fixes #1328 , use Q instead of Z to extract coefficients, and then scale the coefficient with the lcm of their denominators.

sim642 commented 23 hours ago

I should try this on our relational witnesses for Freiburg to see if this produces any new ones we couldn't before.