search

dreal / dreal3

There is a new version of dReal, available at https://github.com/dreal/dreal4
GNU General Public License v3.0
48 stars 36 forks source link

Forall problems in DNF form trigger assertion. #243

Closed cgd8d closed 6 years ago

cgd8d commented 8 years ago

Current behavior is to trigger an assertion in translate_enode_to_exprctr which is rather cryptic; preferred behavior is to provide a more descriptive error, or handle DNF format.

Example input to trigger issue:

(set-logic QF_NRA)
(declare-fun x1 () Real)
(declare-fun forall x2 () Real[7.0, 50.0])
(assert (<= -3.0 x1))
(assert (<= x1 3.14))
(assert
 (forall
  ((x2 Real))
  (or
   (and
    (>= x1 x2)
    (>= x1 0))
   (>= x1 x2))))
(check-sat)
(exit)
soonhokong commented 8 years ago

Thanks, I'll check.

soonho-tri commented 6 years ago

@cgd8d, FYI, we have a new version, dReal4, which can handle this (note: no need to have (declare-fun forall x2 () Real[7.0, 50.0])).