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

Out of memory error on active-standby.kind.lus #23

Closed
mebsout opened this issue Apr 21, 2015 · 2 comments
Closed

Out of memory error on active-standby.kind.lus #23

mebsout opened this issue Apr 21, 2015 · 2 comments

Comments

@mebsout
Copy link

mebsout commented Apr 21, 2015

I'm using jKind v2.1 from the binary releases and java 1.8.0_40 on Mac os x 10.9.5.
jKind crashes on the benchmark active-standby.kind.lus, it looks to be in the frontend because I'm trying to inspect jKind's dump files (in smtlib2 syntax, this is the only reason I use the flag -solver z3).

This is how I run it:

> jkind -scratch -no_inv_gen -no_k_induction -pdr_max 0 -n 0 -scratch -solver z3 active_standby.kind.lus

I get, after about 30s on my machine:

java.lang.OutOfMemoryError: Java heap space
    at java.util.Arrays.copyOf(Arrays.java:3181)
    at java.util.ArrayList.grow(ArrayList.java:261)
    at java.util.ArrayList.ensureExplicitCapacity(ArrayList.java:235)
    at java.util.ArrayList.ensureCapacityInternal(ArrayList.java:227)
    at java.util.ArrayList.add(ArrayList.java:458)
    at jkind.analysis.StaticAnalyzer.checkAlgebraicLoops(StaticAnalyzer.java:324)
    at jkind.analysis.StaticAnalyzer.checkAlgebraicLoops(StaticAnalyzer.java:331)
    ...

For info:

> java -XX:+PrintFlagsFinal -version | grep HeapSize
    uintx ErgoHeapSizeLimit                         = 0                                   {product}
    uintx HeapSizePerGCThread                       = 87241520                            {product}
    uintx InitialHeapSize                          := 134217728                           {product}
    uintx LargePageHeapSizeThreshold                = 134217728                           {product}
    uintx MaxHeapSize                              := 2147483648                          {product}
java version "1.8.0_40"
Java(TM) SE Runtime Environment (build 1.8.0_40-b25)
Java HotSpot(TM) 64-Bit Server VM (build 25.40-b25, mixed mode)
@agacek
Copy link
Collaborator

agacek commented Apr 21, 2015

This is fixed on the master branch by f2efdca. I'll try to make an official release tomorrow which includes this.

@agacek agacek closed this as completed Apr 21, 2015
@mebsout
Copy link
Author

mebsout commented Apr 21, 2015

Okay, thank you!

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