Skip to content
This repository has been archived by the owner on May 11, 2021. It is now read-only.

segfault when 'produce-models' is set #58

Open
robdockins opened this issue Oct 14, 2014 · 0 comments
Open

segfault when 'produce-models' is set #58

robdockins opened this issue Oct 14, 2014 · 0 comments
Assignees
Labels

Comments

@robdockins
Copy link

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 754b19c).

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)
@soonhokong soonhokong added the bug label Oct 14, 2014
@soonhokong soonhokong self-assigned this Oct 14, 2014
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Labels
Projects
None yet
Development

No branches or pull requests

2 participants