dreal / dreal4

Automated Reasoning in Nonlinear Theories of Reals
https://dreal.github.io
Apache License 2.0
150 stars 31 forks source link

[Bug] Unsat with large hexadecimal constant for Ints #284

Open PaulBonnot opened 1 year ago

PaulBonnot commented 1 year ago

dReal return (delta-sat) for the following smt2 code :

(define-fun x() Int 0x7FFFFFFF)
(check-sat)

But (unsat) for :

(define-fun x() Int 0x80000000)
(check-sat)

So there is a bug when handling large hexa constants that are bigger than the maximum integer.

soonhokong commented 1 year ago

Thanks for the report. I'll work on a fix.