Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Segmentation fault #2707

Closed
bkragl opened this issue Nov 17, 2019 · 3 comments
Closed

Segmentation fault #2707

bkragl opened this issue Nov 17, 2019 · 3 comments

Comments

@bkragl
Copy link

bkragl commented Nov 17, 2019

Most recent Z3 segfaults on the following input (generated from Boogie):
smt2.log

I get the following results on Ubuntu 16.04:
4.8.5 (and earlier): unsat
4.8.6: Segmentation fault (without option smt.ARITH.RANDOM_INITIAL_VALUE true: unsat)
4.8.7 (nightly): Segmentation fault (without option smt.CASE_SPLIT 3: unsat)

@NikolajBjorner
Copy link
Contributor

it contains an impressive number of special options.
One has been changed. From now on use:

(set-option :model.compact false)

I don't get the seg faults (yet) locally

@NikolajBjorner
Copy link
Contributor

also, if I disable all options you set. Z3 is much faster

@bkragl
Copy link
Author

bkragl commented Nov 17, 2019

Yeah, these are the options Boogie passes to Z3 by default.

Let me know if you need any other info for reproducing the segfaults, but I just use the binaries for Ubuntu (now I also ran it on Ubuntu 18.04 with the same result).

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants