search

dreal / dreal2

Please check dreal4 instead.
https://github.com/dreal/dreal4
GNU General Public License v3.0
13 stars 15 forks source link

segfault when 'produce-models' is set #58

Open robdockins opened 9 years ago

robdockins commented 9 years ago

Following smt2 input produces a segfault. Segfault disappears if the 'produce-models' option is not set. I get the same result with precompiled dReal (2.14.08) and compiled from git source (commit 754b19c6b22b4004d0a6832892f4e12d752e31de).

System info, OS X (10.9.5):

$ uname -a
Darwin ???? 4.0 Darwin Kernel Version 13.4.0: Sun Aug 17 19:50:11 PDT 2014; root:xnu-2422.115.4~1/RELEASE_X86_64 x86_64
$ clang --version
Apple LLVM version 6.0 (clang-600.0.51) (based on LLVM 3.5svn)
Target: x86_64-apple-darwin13.4.0
Thread model: posix

failing script:

(set-option :produce-models true)
(set-logic QF_NRA)

(declare-fun x0 () Real)
(declare-fun x1 () Real)
(assert (= x1 0.0))

(declare-fun x2 () Bool)
(assert (= x2 (= x0 x0)))
(assert x2)
(check-sat)
(exit)