sambayless / monosat

MonoSAT - An SMT solver for Monotonic Theories
MIT License
108 stars 30 forks source link

Fix an integer overflow issue with the dynamic cut algorithm. #35

Closed NickF0211 closed 2 years ago

NickF0211 commented 2 years ago

Fix an integer overflow issue with the dynamic cut algorithm. Currently, the solver uses an int type TIME variable to stamp node's in the dynamic search tree when computing nodes' distance to terminals. However, after a while, TIME will overflow and will evenutally stamp nodes with negative value. This problem may cause the search tree to form cycles, and stops solving from progressing.

The proposed fix is to change the type of TIME from int to u_int64_t.