Rounding when using very large integers
Opened this issue · 1 comments
rasheedja commented
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 commented
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.