search

usi-verification-and-security / golem

Solver for Constrained Horn Clauses
MIT License
34 stars 7 forks source link

Alethe: Fix evaluation of modulo operation #57

Closed blishko closed 9 months ago

blishko commented 9 months ago

The semantics of the modulo operation on OpenSMT's FastRationals is different than the semantics of modulo as defined by SMT-LIB. This commit changes the evaluation of a modulo operation on two integers to follow the SMT-LIB semantics.

Fixes #55.