Rounding when using very large integers

[rasheedja]

Summary

When using very large integers in dReal, unexpected rounding occurs.

Example

(set-logic QF_NRA)
; 9000000000000000 = 9e15
(assert (not (= (+ 9000000000000000 9000000000000001) (+ 9000000000000000 9000000000000000))))
(check-sat)
(get-model)
(exit)

When running dreal --precision 1e-100 file_name.smt2 on the above program, dReal decides unsat when the result should be delta-sat.

Version Info

dReal version: dReal v4.21.06.2 (Release Build) : delta-complete SMT solver OS:

$ lsb_release -a 
No LSB modules are available.
Distributor ID: Ubuntu
Description:    Ubuntu 20.04.4 LTS
Release:        20.04
Codename:       focal

Compiler:

$ g++ --version
g++ (Ubuntu 9.3.0-17ubuntu1~20.04) 9.3.0
Copyright (C) 2019 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

[soonhokong]

Thanks for the report. This bug is due to the use of IEEE-754 double to represent integer values and constant folding using double. I'll resolve the issue and ping you here later.