Closed lembergerth closed 2 years ago
baierd
commented
2 years ago My approach would be trying to recreate the problem in a JavaSMT program, recreate that using only native Z3 and then either find out why it fails in one and not the other, or ask the Z3 devs. If you want to i can do that over the weekend.
baierd
commented
2 years ago This seems to be caused by our API usage. I can confirm that this crash is happening with JavaSMT API, but it does not happen using native Z3 Java API.
baierd
commented
2 years ago I have further investigated this. There are 2 kinds of Java APIs usable, the default front end that is properly documented and the direct JNI bindings (which we use in JavaSMT). Using the direct JNI bindings i can confirm that this crash persists. The problem seems to the the applyResultDecRef() cleaning up intermediate results of the quantifier elimination in the Z3FormulaCreator line 825. However, since every decRef call also seems to need a incRef call i don't really understand why it is there in the first place as the results are never incRefd. We could simply remove the applyResultDecRef() call in the tactics. This would, in the worst case, result in leaking some memory for multiple tactic applications, which does not happen often. @kfriedberger what do you think? You have more information regarding the Z3 implementation than i do.
lembergerth
commented
2 years ago Thanks for looking into it so well! :-) Please tell me if I can help in any way.
kfriedberger
commented
2 years ago I will take a look. If an intermediate result is still referenced internally in Z3, we should not recrement the reference-counter. In worst case, this might result in a small memory-leak.
If this can be fixed easily (seems so), than we can backport this fix in JavaSMT especally for usage in CPAchecker, because the tool still depends on an older version of JavaSMT (dependency issue with SMTInterpol and LassoRanker, referenced in CPAchecker issue-tracker).
kfriedberger
commented
2 years ago @lembergerth
I have commited JavaSMT in an intermediate version 3.11.0-129-g398a4a02 into the Ivy repository.
I assume you have more tests or benchmarks in CPAchecker for applying quantifier elimination.
Could you (locally) patch CPAchecker with the following patch javasmt_3.11.0-129.patch (hopefully sufficient) to update the version of JavaSMT, and then test whether this issue is fixed (and no other problem was introduced)?
Then we can think about how to properly update JavaSMT in CPAchecker.
lembergerth
commented
2 years ago Thanks! The patch seems to work well. Initially I only had a few small examples, so I also ran integration-predicate-bitprecise.xml with these adjustments:
--- a/test/test-sets/integration-predicate-bitprecise.xml
+++ b/test/test-sets/integration-predicate-bitprecise.xml
@@ -18,6 +18,9 @@ SPDX-License-Identifier: Apache-2.0
<rundefinition>
<option name="-predicateAnalysis"/>
+ <option name="-setprop">cpa.predicate.abstraction.computation=ELIMINATION</option>
+ <option name="-setprop">solver.solver=Z3</option>
+ <option name="-setprop">analysis.algorithm.CEGAR=false</option>
</rundefinition>
<tasks>Results look good with regards to the solver; only a single crash. I think it's unrelated to this issue, but for completeness:
scripts/cpa.sh -noout -heap 2000M -predicateAnalysis -setprop cpa.predicate.abstraction.computation=ELIMINATION -setprop solver.solver=Z3 -setprop analysis.algorithm.CEGAR=false -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -timelimit 60s -stats -spec test/programs/benchmarks/properties/unreach-call.prp -32 test/programs/benchmarks/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c -------------------------------------------------------------------------------- Running CPAchecker with Java heap of size 2000M. Running CPAchecker with default stack size (1024k). Specify a larger value with -stack if needed. Language C detected and set for analysis (CPAMain.detectFrontendLanguageIfNecessary, INFO) Using the following resource limits: CPU-time limit of 60s (ResourceLimitChecker.fromConfiguration, INFO) CPAchecker 2.1.2-svn-39377M / predicateAnalysis (OpenJDK 64-Bit Server VM 11.0.13) started (CPAchecker.run, INFO) Parsing CFA from file(s) "test/programs/benchmarks/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c" (CPAchecker.parse, INFO) Using predicate analysis with Z3 4.8.10.0 and JFactory 1.21. (PredicateCPA:PredicateCPA., INFO) The following configuration options were specified but are not used: cpa.predicate.refinement.performInitialStaticRefinement cegar.refiner (CPAchecker.printConfigurationWarnings, WARNING) Starting analysis ... (CPAchecker.runAlgorithm, INFO) Shutdown requested (The CPU-time limit of 60s has elapsed.), waiting for termination. (ForceTerminationOnShutdown$1.shutdownRequested, WARNING) \# \# A fatal error has been detected by the Java Runtime Environment: \# \# SIGSEGV (0xb) at pc=0x00007f2b8b462d03, pid=2, tid=26 \# \# JRE version: OpenJDK Runtime Environment (11.0.13+8) (build 11.0.13+8-Ubuntu-0ubuntu1.20.04) \# Java VM: OpenJDK 64-Bit Server VM (11.0.13+8-Ubuntu-0ubuntu1.20.04, mixed mode, sharing, tiered, compressed oops, serial gc, linux-amd64) \# Problematic frame: \# C [libz3.so+0xdbbd03] model_evaluator::model_evaluator(model_core&, params_ref const&)+0x33 \# \# No core dump will be written. Core dumps have been disabled. To enable core dumping, try "ulimit -c unlimited" before starting Java again \# \# An error report file with more information is saved as: \# /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/hs_err_pid2.log \# \# If you would like to submit a bug report, please visit: \# https://bugs.launchpad.net/ubuntu/+source/openjdk-lts \# The crash happened outside the Java Virtual Machine in native code. \# See problematic frame for where to report the bug. \# \# \# A fatal error has been detected by the Java Runtime Environment: \# \# SIGSEGV (0xb) at pc=0x00007f2b8b462d03, pid=2, tid=26 \# \# JRE version: OpenJDK Runtime Environment (11.0.13+8) (build 11.0.13+8-Ubuntu-0ubuntu1.20.04) \# Java VM: OpenJDK 64-Bit Server VM (11.0.13+8-Ubuntu-0ubuntu1.20.04, mixed mode, sharing, tiered, compressed oops, serial gc, linux-amd64) \# Problematic frame: \# C [libz3.so+0xdbbd03] model_evaluator::model_evaluator(model_core&, params_ref const&)+0x33 \# \# No core dump will be written. Core dumps have been disabled. To enable core dumping, try "ulimit -c unlimited" before starting Java again \# \# If you would like to submit a bug report, please visit: \# https://bugs.launchpad.net/ubuntu/+source/openjdk-lts \# The crash happened outside the Java Virtual Machine in native code. \# See problematic frame for where to report the bug. \# --------------- S U M M A R Y ------------ Command Line: -XX:+PerfDisableSharedMem -Djava.awt.headless=true -Xss1024k -Xmx2000M -ea org.sosy_lab.cpachecker.cmdline.CPAMain -noout -predicateAnalysis -setprop cpa.predicate.abstraction.computation=ELIMINATION -setprop solver.solver=Z3 -setprop analysis.algorithm.CEGAR=false -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -timelimit 60s -stats -spec test/programs/benchmarks/properties/unreach-call.prp -32 test/programs/benchmarks/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c Host: Intel(R) Xeon(R) CPU E3-1230 v5 @ 3.40GHz, 8 cores, 2G, Ubuntu 20.04.3 LTS Time: Wed Feb 9 11:47:34 2022 CET elapsed time: 61.583083 seconds (0d 0h 1m 1s) --------------- T H R E A D --------------- Current thread (0x00007f2bd0017000): JavaThread "main" [_thread_in_native, id=26, stack(0x00007f2bd6413000,0x00007f2bd6514000)] Stack: [0x00007f2bd6413000,0x00007f2bd6514000], sp=0x00007f2bd6511310, free space=1016k Native frames: (J=compiled Java code, A=aot compiled Java code, j=interpreted, Vv=VM code, C=native code) C [libz3.so+0xdbbd03] model_evaluator::model_evaluator(model_core&, params_ref const&)+0x33 Java frames: (J=compiled Java code, j=interpreted, Vv=VM code) j com.microsoft.z3.Native.INTERNALtacticApply(JJJ)J+0 j com.microsoft.z3.Native.tacticApply(JJJ)J+4 j org.sosy_lab.java_smt.solvers.z3.Z3FormulaCreator.applyTactic(JJLjava/lang/String;)J+41 j org.sosy_lab.java_smt.solvers.z3.Z3FormulaCreator.applyTactics(JLjava/lang/Long;[Ljava/lang/String;)J+38 j org.sosy_lab.java_smt.solvers.z3.Z3QuantifiedFormulaManager.eliminateQuantifiers(Ljava/lang/Long;)Ljava/lang/Long;+23 j org.sosy_lab.java_smt.solvers.z3.Z3QuantifiedFormulaManager.eliminateQuantifiers(Ljava/lang/Object;)Ljava/lang/Object;+5 j org.sosy_lab.java_smt.basicimpl.AbstractQuantifiedFormulaManager.eliminateQuantifiers(Lorg/sosy_lab/java_smt/api/BooleanFormula;)Lorg/sosy_lab/java_smt/api/BooleanFormula;+7 j org.sosy_lab.cpachecker.util.predicates.smt.QuantifiedFormulaManagerView.eliminateQuantifiers(Lorg/sosy_lab/java_smt/api/BooleanFormula;)Lorg/sosy_lab/java_smt/api/BooleanFormula;+5 j org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.eliminateVariables(Lorg/sosy_lab/java_smt/api/BooleanFormula;Lcom/google/common/base/Predicate;)Lorg/sosy_lab/java_smt/api/BooleanFormula;+57 j org.sosy_lab.cpachecker.util.predicates.smt.FormulaManagerView.eliminateDeadVariables(Lorg/sosy_lab/java_smt/api/BooleanFormula;Lorg/sosy_lab/cpachecker/util/predicates/pathformula/SSAMap;)Lorg/sosy_lab/java_smt/api/BooleanFormula;+14 j org.sosy_lab.cpachecker.cpa.predicate.PredicateAbstractionManager.buildAbstraction(Ljava/util/Collection;Ljava/util/Optional;Lorg/sosy_lab/cpachecker/util/predicates/AbstractionFormula;Lorg/sosy_lab/cpachecker/util/predicates/pathformula/PathFormula;Ljava/util/Collection;)Lorg/sosy_lab/cpachecker/util/predicates/AbstractionFormula;+892 j org.sosy_lab.cpachecker.cpa.predicate.PredicatePrecisionAdjustment.computeAbstraction(Lorg/sosy_lab/cpachecker/cpa/predicate/PredicateAbstractState;Lorg/sosy_lab/cpachecker/cpa/predicate/PredicatePrecision;Ljava/util/Collection;Lorg/sosy_lab/cpachecker/core/interfaces/AbstractState;)Ljava/util/Optional;+356 j org.sosy_lab.cpachecker.cpa.predicate.PredicatePrecisionAdjustment.prec(Lorg/sosy_lab/cpachecker/core/interfaces/AbstractState;Lorg/sosy_lab/cpachecker/core/interfaces/Precision;Lorg/sosy_lab/cpachecker/core/reachedset/UnmodifiableReachedSet;Lcom/google/common/base/Function;Lorg/sosy_lab/cpachecker/core/interfaces/AbstractState;)Ljava/util/Optional;+82 J 3730 c1 org.sosy_lab.cpachecker.cpa.composite.CompositePrecisionAdjustment.prec(Lorg/sosy_lab/cpachecker/core/interfaces/AbstractState;Lorg/sosy_lab/cpachecker/core/interfaces/Precision;Lorg/sosy_lab/cpachecker/core/reachedset/UnmodifiableReachedSet;Lcom/google/common/base/Function;Lorg/sosy_lab/cpachecker/core/interfaces/AbstractState;)Ljava/util/Optional; (336 bytes) @ 0x00007f2bb957c03c [0x00007f2bb957a7c0+0x000000000000187c] j org.sosy_lab.cpachecker.cpa.arg.ARGPrecisionAdjustment.prec(Lorg/sosy_lab/cpachecker/cpa/arg/ARGState;Lorg/sosy_lab/cpachecker/core/interfaces/Precision;Lorg/sosy_lab/cpachecker/core/reachedset/UnmodifiableReachedSet;Lcom/google/common/base/Function;Lorg/sosy_lab/cpachecker/core/interfaces/AbstractState;)Ljava/util/Optional;+66 j org.sosy_lab.cpachecker.cpa.arg.ARGPrecisionAdjustment.prec(Lorg/sosy_lab/cpachecker/core/interfaces/AbstractState;Lorg/sosy_lab/cpachecker/core/interfaces/Precision;Lorg/sosy_lab/cpachecker/core/reachedset/UnmodifiableReachedSet;Lcom/google/common/base/Function;Lorg/sosy_lab/cpachecker/core/interfaces/AbstractState;)Ljava/util/Optional;+22 j org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.handleState(Lorg/sosy_lab/cpachecker/core/interfaces/AbstractState;Lorg/sosy_lab/cpachecker/core/interfaces/Precision;Lorg/sosy_lab/cpachecker/core/reachedset/ReachedSet;)Z+358 j org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run0(Lorg/sosy_lab/cpachecker/core/reachedset/ReachedSet;)Lorg/sosy_lab/cpachecker/core/algorithm/Algorithm$AlgorithmStatus;+136 j org.sosy_lab.cpachecker.core.algorithm.CPAAlgorithm.run(Lorg/sosy_lab/cpachecker/core/reachedset/ReachedSet;)Lorg/sosy_lab/cpachecker/core/algorithm/Algorithm$AlgorithmStatus;+12 j org.sosy_lab.cpachecker.core.CPAchecker.runAlgorithm(Lorg/sosy_lab/cpachecker/core/algorithm/Algorithm;Lorg/sosy_lab/cpachecker/core/reachedset/ReachedSet;Lorg/sosy_lab/cpachecker/core/MainCPAStatistics;)Lorg/sosy_lab/cpachecker/core/algorithm/Algorithm$AlgorithmStatus;+60 j org.sosy_lab.cpachecker.core.CPAchecker.run(Ljava/util/List;)Lorg/sosy_lab/cpachecker/core/CPAcheckerResult;+399 j org.sosy_lab.cpachecker.cmdline.CPAMain.main([Ljava/lang/String;)V+365 v ~StubRoutines::call_stub siginfo: si_signo: 11 (SIGSEGV), si_code: 1 (SEGV_MAPERR), si_addr: 0x0000000000000008 Register to memory mapping: RAX=0x00007f2b7d196d08 points into unknown readable memory: 0x00007f2b7d2140b0 | b0 40 21 7d 2b 7f 00 00 RBX=0x00007f2bd0759ae8 points into unknown readable memory: 0x00007f2b8bfdc898 | 98 c8 fd 8b 2b 7f 00 00 RCX=0x0000000000000791 is an unknown value RDX=0x000055b816038a60 points into unknown readable memory: 0x0000000000000003 | 03 00 00 00 00 00 00 00 RSP=0x00007f2bd6511310 is pointing into the stack for thread: 0x00007f2bd0017000 RBP=0x00007f2b7d1bbe88 points into unknown readable memory: 0x0000000000000000 | 00 00 00 00 00 00 00 00 RSI=0x00007f2bd0000080 points into unknown readable memory: 0x00007f2b7d5780b0 | b0 80 57 7d 2b 7f 00 00 RDI=0x00007f2b8bffbfe0: in /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/libz3.so at 0x00007f2b8a6a7000 R8 =0x00007f2b7d196d00 points into unknown readable memory: 0x0000000000000780 | 80 07 00 00 00 00 00 00 R9 =0x00007f2bd0000510 points into unknown readable memory: 0x00007f2b7d233ff0 | f0 3f 23 7d 2b 7f 00 00 R10=0x00007f2bd00008d0 points into unknown readable memory: 0x0006000700070005 | 05 00 07 00 07 00 06 00 R11=0x00007f2bd0000080 points into unknown readable memory: 0x00007f2b7d5780b0 | b0 80 57 7d 2b 7f 00 00 R12=0x0 is NULL R13=0x00007f2bd6511440 is pointing into the stack for thread: 0x00007f2bd0017000 R14=0x00007f2bd6511440 is pointing into the stack for thread: 0x00007f2bd0017000 R15=0x00007f2bd3c88b28 points into unknown readable memory: 0x00007f2bd2c5fe50 | 50 fe c5 d2 2b 7f 00 00 Registers: RAX=0x00007f2b7d196d08, RBX=0x00007f2bd0759ae8, RCX=0x0000000000000791, RDX=0x000055b816038a60 RSP=0x00007f2bd6511310, RBP=0x00007f2b7d1bbe88, RSI=0x00007f2bd0000080, RDI=0x00007f2b8bffbfe0 R8 =0x00007f2b7d196d00, R9 =0x00007f2bd0000510, R10=0x00007f2bd00008d0, R11=0x00007f2bd0000080 R12=0x0000000000000000, R13=0x00007f2bd6511440, R14=0x00007f2bd6511440, R15=0x00007f2bd3c88b28 RIP=0x00007f2b8b462d03, EFLAGS=0x0000000000010206, CSGSFS=0x002b000000000033, ERR=0x0000000000000004 TRAPNO=0x000000000000000e Top of Stack: (sp=0x00007f2bd6511310) 0x00007f2bd6511310: 00007f2bd086e0f8 00007f2b7d1578e0 0x00007f2bd6511320: 00007f2bd0661018 00007f2b7d1bbe88 0x00007f2bd6511330: 00007f2bd3c88b28 0000008700000d4a 0x00007f2bd6511340: 00007f2b7d1bcc38 0000000000000000 Instructions: (pc=0x00007f2b8b462d03) 0x00007f2b8b462c03: c5 eb b1 48 8b bb 88 02 00 00 48 89 c5 48 85 ff 0x00007f2b8b462c13: 74 b3 e8 e6 83 67 00 eb ac 48 89 c5 48 8d bb 20 0x00007f2b8b462c23: 02 00 00 e8 05 07 88 ff e9 61 ff ff ff 48 8b bb 0x00007f2b8b462c33: 38 02 00 00 48 89 c5 48 85 ff 74 e0 e8 bc 83 67 0x00007f2b8b462c43: 00 eb d9 48 89 c5 e9 7a ff ff ff 4c 89 ff 48 89 0x00007f2b8b462c53: c5 e8 27 fd 74 ff e9 33 ff ff ff 48 8b 7c 24 08 0x00007f2b8b462c63: 48 89 c5 e8 b5 47 15 00 48 8d bb d8 04 00 00 e8 0x00007f2b8b462c73: b9 9d 31 ff 48 8b 3c 24 e8 60 45 64 00 e9 dc fe 0x00007f2b8b462c83: ff ff 4c 89 e7 48 89 c5 e8 50 45 64 00 eb d9 48 0x00007f2b8b462c93: 89 c5 eb d4 48 89 c5 eb db 4c 89 e7 48 89 c5 e8 0x00007f2b8b462ca3: 39 45 64 00 e9 bf fe ff ff 4c 89 e7 48 89 c5 e8 0x00007f2b8b462cb3: 29 45 64 00 e9 bb fe ff ff 48 89 c5 e9 bd fe ff 0x00007f2b8b462cc3: ff 48 89 c5 e9 63 fe ff ff 0f 1f 40 00 41 57 41 0x00007f2b8b462cd3: 56 41 55 41 54 49 89 f4 55 53 49 89 d5 48 83 ec 0x00007f2b8b462ce3: 78 48 89 7c 24 18 bf 78 07 00 00 64 48 8b 04 25 0x00007f2b8b462cf3: 28 00 00 00 48 89 44 24 68 31 c0 e8 0d 84 67 00 0x00007f2b8b462d03: 49 8b 6c 24 08 48 89 c7 31 d2 48 89 c3 4c 8d b3 0x00007f2b8b462d13: 90 00 00 00 48 89 ee e8 c1 44 0c 00 48 8d 05 1a 0x00007f2b8b462d23: 34 b8 00 31 d2 48 89 ee 4c 89 f7 c7 83 80 00 00 0x00007f2b8b462d33: 00 00 00 00 00 48 c7 83 88 00 00 00 00 00 00 00 0x00007f2b8b462d43: 48 89 03 48 8d 83 d0 01 00 00 48 89 43 78 e8 8a 0x00007f2b8b462d53: 44 0c 00 48 8d 05 8b 37 b8 00 48 8d bb 18 01 00 0x00007f2b8b462d63: 00 31 d2 48 89 ee 48 c7 83 08 01 00 00 00 00 00 0x00007f2b8b462d73: 00 c7 83 10 01 00 00 00 00 00 00 48 83 c0 10 48 0x00007f2b8b462d83: 89 83 90 00 00 00 e8 52 44 0c 00 48 8d 05 7b 37 0x00007f2b8b462d93: b8 00 48 89 ab a0 01 00 00 4c 89 ee 48 89 ab b0 0x00007f2b8b462da3: 01 00 00 48 89 ab c0 01 00 00 49 8b 6c 24 08 48 0x00007f2b8b462db3: c7 83 98 01 00 00 00 00 00 00 48 83 c0 10 48 c7 0x00007f2b8b462dc3: 83 a8 01 00 00 00 00 00 00 48 c7 83 b8 01 00 00 0x00007f2b8b462dd3: 00 00 00 00 48 89 83 18 01 00 00 48 8d 05 7b 33 0x00007f2b8b462de3: b8 00 48 c7 83 c8 01 00 00 00 00 00 00 48 89 ab 0x00007f2b8b462df3: d0 01 00 00 4c 89 a3 d8 01 00 00 48 89 03 48 8d Stack slot to memory mapping: stack at sp + 0 slots: 0x00007f2bd086e0f8 points into unknown readable memory: 0x00007f2b8bfe7638 | 38 76 fe 8b 2b 7f 00 00 stack at sp + 1 slots: 0x00007f2b7d1578e0 points into unknown readable memory: 0x00007f2bd3abcdf8 | f8 cd ab d3 2b 7f 00 00 stack at sp + 2 slots: 0x00007f2bd0661018 points into unknown readable memory: 0x0000000000000002 | 02 00 00 00 00 00 00 00 stack at sp + 3 slots: 0x00007f2b7d1bbe88 points into unknown readable memory: 0x0000000000000000 | 00 00 00 00 00 00 00 00 stack at sp + 4 slots: 0x00007f2bd3c88b28 points into unknown readable memory: 0x00007f2bd2c5fe50 | 50 fe c5 d2 2b 7f 00 00 stack at sp + 5 slots: 0x0000008700000d4a is an unknown value stack at sp + 6 slots: 0x00007f2b7d1bcc38 points into unknown readable memory: 0x00007f2bd00008d0 | d0 08 00 d0 2b 7f 00 00 stack at sp + 7 slots: 0x0 is NULL --------------- P R O C E S S --------------- Threads class SMR info: _java_thread_list=0x00007f2bd050a8a0, length=11, elements={ 0x00007f2bd0017000, 0x00007f2bd0052000, 0x00007f2bd0054000, 0x00007f2bd005b000, 0x00007f2bd005d000, 0x00007f2bd005f000, 0x00007f2bd0061000, 0x00007f2bd0063000, 0x00007f2bd0075800, 0x00007f2bd0509000, 0x00007f2b90004000 } Java Threads: ( => current thread ) =>0x00007f2bd0017000 JavaThread "main" [_thread_in_native, id=26, stack(0x00007f2bd6413000,0x00007f2bd6514000)] 0x00007f2bd0052000 JavaThread "Reference Handler" daemon [_thread_blocked, id=30, stack(0x00007f2bd5005000,0x00007f2bd5106000)] 0x00007f2bd0054000 JavaThread "Finalizer" daemon [_thread_blocked, id=31, stack(0x00007f2bd4f04000,0x00007f2bd5005000)] 0x00007f2bd005b000 JavaThread "Signal Dispatcher" daemon [_thread_blocked, id=32, stack(0x00007f2bd4aff000,0x00007f2bd4c00000)] 0x00007f2bd005d000 JavaThread "Service Thread" daemon [_thread_blocked, id=33, stack(0x00007f2bd49fe000,0x00007f2bd4aff000)] 0x00007f2bd005f000 JavaThread "C2 CompilerThread0" daemon [_thread_blocked, id=34, stack(0x00007f2bd48fd000,0x00007f2bd49fe000)] 0x00007f2bd0061000 JavaThread "C1 CompilerThread0" daemon [_thread_blocked, id=35, stack(0x00007f2bd47fc000,0x00007f2bd48fd000)] 0x00007f2bd0063000 JavaThread "Sweeper thread" daemon [_thread_blocked, id=36, stack(0x00007f2bd46fb000,0x00007f2bd47fc000)] 0x00007f2bd0075800 JavaThread "Common-Cleaner" daemon [_thread_blocked, id=38, stack(0x00007f2bd44f8000,0x00007f2bd45f9000)] 0x00007f2bd0509000 JavaThread "CPAchecker memory statistics collector" daemon [_thread_blocked, id=40, stack(0x00007f2bd428f000,0x00007f2bd4390000)] 0x00007f2b90004000 JavaThread "ForceTerminationOnShutdown" daemon [_thread_blocked, id=41, stack(0x00007f2b89ea5000,0x00007f2b89fa6000)] Other Threads: 0x00007f2bd004f000 VMThread "VM Thread" [stack: 0x00007f2bd5108000,0x00007f2bd5208000] [id=29] 0x00007f2bd00a3000 WatcherThread [stack: 0x00007f2bd45fb000,0x00007f2bd46fb000] [id=37] Threads with active compile tasks: VM state:not at safepoint (normal execution) VM Mutex/Monitor currently owned by a thread: None Heap address: 0x0000000083000000, size: 2000 MB, Compressed Oops mode: 32-bit Narrow klass base: 0x0000000800000000, Narrow klass shift: 3 Compressed class space size: 1073741824 Address: 0x0000000840000000 Heap: def new generation total 12096K, used 9235K [0x0000000083000000, 0x0000000083d20000, 0x00000000acaa0000) eden space 10752K, 80% used [0x0000000083000000, 0x000000008386dc08, 0x0000000083a80000) from space 1344K, 44% used [0x0000000083bd0000, 0x0000000083c67048, 0x0000000083d20000) to space 1344K, 0% used [0x0000000083a80000, 0x0000000083a80000, 0x0000000083bd0000) tenured generation total 26844K, used 18085K [0x00000000acaa0000, 0x00000000ae4d7000, 0x0000000100000000) the space 26844K, 67% used [0x00000000acaa0000, 0x00000000adc49528, 0x00000000adc49600, 0x00000000ae4d7000) Metaspace used 23218K, capacity 23987K, committed 24112K, reserved 1071104K class space used 2568K, capacity 2886K, committed 2944K, reserved 1048576K Card table byte_map: [0x00007f2bd5de9000,0x00007f2bd61d2000] _byte_map_base: 0x00007f2bd59d1000 Polling page: 0x00007f2bd63c6000 Metaspace: Usage: Non-class: 20.61 MB capacity, 20.17 MB ( 98%) used, 365.47 KB ( 2%) free+waste, 86.19 KB ( <1%) overhead. Class: 2.82 MB capacity, 2.51 MB ( 89%) used, 275.80 KB ( 10%) free+waste, 41.50 KB ( 1%) overhead. Both: 23.42 MB capacity, 22.67 MB ( 97%) used, 641.27 KB ( 3%) free+waste, 127.69 KB ( <1%) overhead. Virtual space: Non-class space: 22.00 MB reserved, 20.67 MB ( 94%) committed Class space: 1.00 GB reserved, 2.88 MB ( <1%) committed Both: 1.02 GB reserved, 23.55 MB ( 2%) committed Chunk freelists: Non-Class: 43.00 KB Class: 0 bytes Both: 43.00 KB MaxMetaspaceSize: unlimited CompressedClassSpaceSize: 1.00 GB Initial GC threshold: 20.80 MB Current GC threshold: 34.66 MB CDS: on CodeHeap 'non-profiled nmethods': size=120036Kb used=1332Kb max_used=1332Kb free=118703Kb bounds [0x00007f2bc031a000, 0x00007f2bc058a000, 0x00007f2bc7853000] CodeHeap 'profiled nmethods': size=120032Kb used=8528Kb max_used=8528Kb free=111503Kb bounds [0x00007f2bb8de2000, 0x00007f2bb9642000, 0x00007f2bc031a000] CodeHeap 'non-nmethods': size=5692Kb used=1275Kb max_used=1293Kb free=4416Kb bounds [0x00007f2bb8853000, 0x00007f2bb8ac3000, 0x00007f2bb8de2000] total_blobs=4564 nmethods=3989 adapters=489 compilation: enabled stopped_count=0, restarted_count=0 full_count=0 Compilation events (20 events): Event: 40.849 Thread 0x00007f2bd0061000 3992 3 sun.reflect.misc.Trampoline::ensureInvocableMethod (53 bytes) Event: 40.849 Thread 0x00007f2bd0061000 nmethod 3992 0x00007f2bb962ca10 code [0x00007f2bb962cc40, 0x00007f2bb962d3b0] Event: 51.769 Thread 0x00007f2bd0061000 3993 3 java.util.concurrent.locks.ReentrantReadWriteLock$Sync::tryReleaseShared (146 bytes) Event: 51.770 Thread 0x00007f2bd0061000 nmethod 3993 0x00007f2bb962d690 code [0x00007f2bb962d960, 0x00007f2bb962e980] Event: 52.069 Thread 0x00007f2bd0061000 3994 ! 3 com.sun.jmx.mbeanserver.MBeanIntrospector::invokeM (44 bytes) Event: 52.070 Thread 0x00007f2bd0061000 nmethod 3994 0x00007f2bb962ef10 code [0x00007f2bb962f120, 0x00007f2bb962f580] Event: 52.070 Thread 0x00007f2bd0061000 3995 3 com.sun.jmx.mbeanserver.MXBeanIntrospector::invokeM2 (13 bytes) Event: 52.070 Thread 0x00007f2bd0061000 nmethod 3995 0x00007f2bb962f790 code [0x00007f2bb962f960, 0x00007f2bb962fd40] Event: 52.070 Thread 0x00007f2bd0061000 3996 3 com.sun.jmx.mbeanserver.MXBeanIntrospector::invokeM2 (12 bytes) Event: 52.070 Thread 0x00007f2bd0061000 nmethod 3996 0x00007f2bb962fe90 code [0x00007f2bb96300c0, 0x00007f2bb9630980] Event: 52.070 Thread 0x00007f2bd0061000 3997 ! 3 com.sun.jmx.mbeanserver.ConvertingMethod::invokeWithOpenReturn (35 bytes) Event: 52.071 Thread 0x00007f2bd0061000 nmethod 3997 0x00007f2bb9630c90 code [0x00007f2bb9630f60, 0x00007f2bb96321d0] Event: 52.071 Thread 0x00007f2bd0061000 3998 3 com.sun.jmx.mbeanserver.MXBeanLookup::getLookup (10 bytes) Event: 52.071 Thread 0x00007f2bd0061000 nmethod 3998 0x00007f2bb9632810 code [0x00007f2bb96329e0, 0x00007f2bb9632c80] Event: 52.071 Thread 0x00007f2bd0061000 3999 ! 3 com.sun.jmx.mbeanserver.ConvertingMethod::invokeWithOpenReturn (84 bytes) Event: 52.072 Thread 0x00007f2bd0061000 nmethod 3999 0x00007f2bb9632d10 code [0x00007f2bb9632f80, 0x00007f2bb9633620] Event: 52.072 Thread 0x00007f2bd0061000 4000 3 com.sun.jmx.mbeanserver.ConvertingMethod::fromOpenParameters (50 bytes) Event: 52.072 Thread 0x00007f2bd0061000 nmethod 4000 0x00007f2bb9633a10 code [0x00007f2bb9633c00, 0x00007f2bb96341a0] Event: 52.072 Thread 0x00007f2bd0061000 4001 ! 3 sun.reflect.misc.MethodUtil::invoke (111 bytes) Event: 52.073 Thread 0x00007f2bd0061000 nmethod 4001 0x00007f2bb9634390 code [0x00007f2bb9634660, 0x00007f2bb9635c20] GC Heap History (20 events): Event: 1.830 GC heap before {Heap before GC invocations=3 (full 0): def new generation total 11648K, used 11648K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 100% used [0x0000000083000000, 0x0000000083a20000, 0x0000000083a20000) from space 1280K, 100% used [0x0000000083b60000, 0x0000000083ca0000, 0x0000000083ca0000) to space 1280K, 0% used [0x0000000083a20000, 0x0000000083a20000, 0x0000000083b60000) tenured generation total 25984K, used 7392K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 28% used [0x00000000acaa0000, 0x00000000ad1d80d0, 0x00000000ad1d8200, 0x00000000ae400000) Metaspace used 9345K, capacity 9646K, committed 9984K, reserved 1058816K class space used 1076K, capacity 1182K, committed 1280K, reserved 1048576K } Event: 1.834 GC heap after {Heap after GC invocations=4 (full 0): def new generation total 11648K, used 1276K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 0% used [0x0000000083000000, 0x0000000083000000, 0x0000000083a20000) from space 1280K, 99% used [0x0000000083a20000, 0x0000000083b5f3f8, 0x0000000083b60000) to space 1280K, 0% used [0x0000000083b60000, 0x0000000083b60000, 0x0000000083ca0000) tenured generation total 25984K, used 8211K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 31% used [0x00000000acaa0000, 0x00000000ad2a4fd8, 0x00000000ad2a5000, 0x00000000ae400000) Metaspace used 9345K, capacity 9646K, committed 9984K, reserved 1058816K class space used 1076K, capacity 1182K, committed 1280K, reserved 1048576K } Event: 2.041 GC heap before {Heap before GC invocations=4 (full 0): def new generation total 11648K, used 11644K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 100% used [0x0000000083000000, 0x0000000083a20000, 0x0000000083a20000) from space 1280K, 99% used [0x0000000083a20000, 0x0000000083b5f3f8, 0x0000000083b60000) to space 1280K, 0% used [0x0000000083b60000, 0x0000000083b60000, 0x0000000083ca0000) tenured generation total 25984K, used 8211K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 31% used [0x00000000acaa0000, 0x00000000ad2a4fd8, 0x00000000ad2a5000, 0x00000000ae400000) Metaspace used 9547K, capacity 9820K, committed 9984K, reserved 1058816K class space used 1092K, capacity 1218K, committed 1280K, reserved 1048576K } Event: 2.048 GC heap after {Heap after GC invocations=5 (full 0): def new generation total 11648K, used 1279K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 0% used [0x0000000083000000, 0x0000000083000000, 0x0000000083a20000) from space 1280K, 99% used [0x0000000083b60000, 0x0000000083c9fff8, 0x0000000083ca0000) to space 1280K, 0% used [0x0000000083a20000, 0x0000000083a20000, 0x0000000083b60000) tenured generation total 25984K, used 10804K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 41% used [0x00000000acaa0000, 0x00000000ad52d378, 0x00000000ad52d400, 0x00000000ae400000) Metaspace used 9547K, capacity 9820K, committed 9984K, reserved 1058816K class space used 1092K, capacity 1218K, committed 1280K, reserved 1048576K } Event: 2.333 GC heap before {Heap before GC invocations=5 (full 0): def new generation total 11648K, used 11647K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 100% used [0x0000000083000000, 0x0000000083a20000, 0x0000000083a20000) from space 1280K, 99% used [0x0000000083b60000, 0x0000000083c9fff8, 0x0000000083ca0000) to space 1280K, 0% used [0x0000000083a20000, 0x0000000083a20000, 0x0000000083b60000) tenured generation total 25984K, used 10804K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 41% used [0x00000000acaa0000, 0x00000000ad52d378, 0x00000000ad52d400, 0x00000000ae400000) Metaspace used 10753K, capacity 11107K, committed 11392K, reserved 1058816K class space used 1192K, capacity 1347K, committed 1408K, reserved 1048576K } Event: 2.335 GC heap after {Heap after GC invocations=6 (full 0): def new generation total 11648K, used 647K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 0% used [0x0000000083000000, 0x0000000083000000, 0x0000000083a20000) from space 1280K, 50% used [0x0000000083a20000, 0x0000000083ac1d08, 0x0000000083b60000) to space 1280K, 0% used [0x0000000083b60000, 0x0000000083b60000, 0x0000000083ca0000) tenured generation total 25984K, used 11216K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 43% used [0x00000000acaa0000, 0x00000000ad594390, 0x00000000ad594400, 0x00000000ae400000) Metaspace used 10753K, capacity 11107K, committed 11392K, reserved 1058816K class space used 1192K, capacity 1347K, committed 1408K, reserved 1048576K } Event: 2.766 GC heap before {Heap before GC invocations=6 (full 0): def new generation total 11648K, used 11015K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 100% used [0x0000000083000000, 0x0000000083a20000, 0x0000000083a20000) from space 1280K, 50% used [0x0000000083a20000, 0x0000000083ac1d08, 0x0000000083b60000) to space 1280K, 0% used [0x0000000083b60000, 0x0000000083b60000, 0x0000000083ca0000) tenured generation total 25984K, used 11216K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 43% used [0x00000000acaa0000, 0x00000000ad594390, 0x00000000ad594400, 0x00000000ae400000) Metaspace used 13216K, capacity 13574K, committed 13696K, reserved 1060864K class space used 1487K, capacity 1639K, committed 1664K, reserved 1048576K } Event: 2.770 GC heap after {Heap after GC invocations=7 (full 0): def new generation total 11648K, used 814K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 0% used [0x0000000083000000, 0x0000000083000000, 0x0000000083a20000) from space 1280K, 63% used [0x0000000083b60000, 0x0000000083c2ba30, 0x0000000083ca0000) to space 1280K, 0% used [0x0000000083a20000, 0x0000000083a20000, 0x0000000083b60000) tenured generation total 25984K, used 11854K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 45% used [0x00000000acaa0000, 0x00000000ad633a50, 0x00000000ad633c00, 0x00000000ae400000) Metaspace used 13216K, capacity 13574K, committed 13696K, reserved 1060864K class space used 1487K, capacity 1639K, committed 1664K, reserved 1048576K } Event: 3.304 GC heap before {Heap before GC invocations=7 (full 0): def new generation total 11648K, used 11182K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 100% used [0x0000000083000000, 0x0000000083a20000, 0x0000000083a20000) from space 1280K, 63% used [0x0000000083b60000, 0x0000000083c2ba30, 0x0000000083ca0000) to space 1280K, 0% used [0x0000000083a20000, 0x0000000083a20000, 0x0000000083b60000) tenured generation total 25984K, used 11854K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 45% used [0x00000000acaa0000, 0x00000000ad633a50, 0x00000000ad633c00, 0x00000000ae400000) Metaspace used 14697K, capacity 15155K, committed 15232K, reserved 1062912K class space used 1668K, capacity 1870K, committed 1920K, reserved 1048576K } Event: 3.310 GC heap after {Heap after GC invocations=8 (full 0): def new generation total 11648K, used 1280K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 0% used [0x0000000083000000, 0x0000000083000000, 0x0000000083a20000) from space 1280K, 100% used [0x0000000083a20000, 0x0000000083b60000, 0x0000000083b60000) to space 1280K, 0% used [0x0000000083b60000, 0x0000000083b60000, 0x0000000083ca0000) tenured generation total 25984K, used 12993K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 50% used [0x00000000acaa0000, 0x00000000ad750418, 0x00000000ad750600, 0x00000000ae400000) Metaspace used 14697K, capacity 15155K, committed 15232K, reserved 1062912K class space used 1668K, capacity 1870K, committed 1920K, reserved 1048576K } Event: 3.691 GC heap before {Heap before GC invocations=8 (full 0): def new generation total 11648K, used 11648K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 100% used [0x0000000083000000, 0x0000000083a20000, 0x0000000083a20000) from space 1280K, 100% used [0x0000000083a20000, 0x0000000083b60000, 0x0000000083b60000) to space 1280K, 0% used [0x0000000083b60000, 0x0000000083b60000, 0x0000000083ca0000) tenured generation total 25984K, used 12993K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 50% used [0x00000000acaa0000, 0x00000000ad750418, 0x00000000ad750600, 0x00000000ae400000) Metaspace used 15384K, capacity 15926K, committed 16128K, reserved 1062912K class space used 1758K, capacity 1997K, committed 2048K, reserved 1048576K } Event: 3.696 GC heap after {Heap after GC invocations=9 (full 0): def new generation total 11648K, used 706K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 0% used [0x0000000083000000, 0x0000000083000000, 0x0000000083a20000) from space 1280K, 55% used [0x0000000083b60000, 0x0000000083c10a10, 0x0000000083ca0000) to space 1280K, 0% used [0x0000000083a20000, 0x0000000083a20000, 0x0000000083b60000) tenured generation total 25984K, used 14176K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 54% used [0x00000000acaa0000, 0x00000000ad8781e8, 0x00000000ad878200, 0x00000000ae400000) Metaspace used 15384K, capacity 15926K, committed 16128K, reserved 1062912K class space used 1758K, capacity 1997K, committed 2048K, reserved 1048576K } Event: 4.023 GC heap before {Heap before GC invocations=9 (full 0): def new generation total 11648K, used 11074K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 100% used [0x0000000083000000, 0x0000000083a20000, 0x0000000083a20000) from space 1280K, 55% used [0x0000000083b60000, 0x0000000083c10a10, 0x0000000083ca0000) to space 1280K, 0% used [0x0000000083a20000, 0x0000000083a20000, 0x0000000083b60000) tenured generation total 25984K, used 14176K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 54% used [0x00000000acaa0000, 0x00000000ad8781e8, 0x00000000ad878200, 0x00000000ae400000) Metaspace used 16487K, capacity 17027K, committed 17280K, reserved 1064960K class space used 1897K, capacity 2129K, committed 2176K, reserved 1048576K } Event: 4.026 GC heap after {Heap after GC invocations=10 (full 0): def new generation total 11648K, used 526K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 0% used [0x0000000083000000, 0x0000000083000000, 0x0000000083a20000) from space 1280K, 41% used [0x0000000083a20000, 0x0000000083aa3948, 0x0000000083b60000) to space 1280K, 0% used [0x0000000083b60000, 0x0000000083b60000, 0x0000000083ca0000) tenured generation total 25984K, used 14761K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 56% used [0x00000000acaa0000, 0x00000000ad90a7a8, 0x00000000ad90a800, 0x00000000ae400000) Metaspace used 16487K, capacity 17027K, committed 17280K, reserved 1064960K class space used 1897K, capacity 2129K, committed 2176K, reserved 1048576K } Event: 4.470 GC heap before {Heap before GC invocations=10 (full 0): def new generation total 11648K, used 10894K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 100% used [0x0000000083000000, 0x0000000083a20000, 0x0000000083a20000) from space 1280K, 41% used [0x0000000083a20000, 0x0000000083aa3948, 0x0000000083b60000) to space 1280K, 0% used [0x0000000083b60000, 0x0000000083b60000, 0x0000000083ca0000) tenured generation total 25984K, used 14761K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 56% used [0x00000000acaa0000, 0x00000000ad90a7a8, 0x00000000ad90a800, 0x00000000ae400000) Metaspace used 18953K, capacity 19558K, committed 19712K, reserved 1067008K class space used 2182K, capacity 2437K, committed 2560K, reserved 1048576K } Event: 4.473 GC heap after {Heap after GC invocations=11 (full 0): def new generation total 11648K, used 1279K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 0% used [0x0000000083000000, 0x0000000083000000, 0x0000000083a20000) from space 1280K, 99% used [0x0000000083b60000, 0x0000000083c9fff8, 0x0000000083ca0000) to space 1280K, 0% used [0x0000000083a20000, 0x0000000083a20000, 0x0000000083b60000) tenured generation total 25984K, used 14831K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 57% used [0x00000000acaa0000, 0x00000000ad91bc10, 0x00000000ad91be00, 0x00000000ae400000) Metaspace used 18953K, capacity 19558K, committed 19712K, reserved 1067008K class space used 2182K, capacity 2437K, committed 2560K, reserved 1048576K } Event: 4.647 GC heap before {Heap before GC invocations=11 (full 0): def new generation total 11648K, used 7825K [0x0000000083000000, 0x0000000083ca0000, 0x00000000acaa0000) eden space 10368K, 63% used [0x0000000083000000, 0x0000000083664548, 0x0000000083a20000) from space 1280K, 99% used [0x0000000083b60000, 0x0000000083c9fff8, 0x0000000083ca0000) to space 1280K, 0% used [0x0000000083a20000, 0x0000000083a20000, 0x0000000083b60000) tenured generation total 25984K, used 14831K [0x00000000acaa0000, 0x00000000ae400000, 0x0000000100000000) the space 25984K, 57% used [0x00000000acaa0000, 0x00000000ad91bc10, 0x00000000ad91be00, 0x00000000ae400000) Metaspace used 20472K, capacity 21143K, committed 21296K, reserved 1069056K class space used 2318K, capacity 2605K, committed 2688K, reserved 1048576K } Event: 4.676 GC heap after {Heap after GC invocations=12 (full 1): def new generation total 12096K, used 0K [0x0000000083000000, 0x0000000083d20000, 0x00000000acaa0000) eden space 10752K, 0% used [0x0000000083000000, 0x0000000083000000, 0x0000000083a80000) from space 1344K, 0% used [0x0000000083a80000, 0x0000000083a80000, 0x0000000083bd0000) to space 1344K, 0% used [0x0000000083bd0000, 0x0000000083bd0000, 0x0000000083d20000) tenured generation total 26844K, used 16105K [0x00000000acaa0000, 0x00000000ae4d7000, 0x0000000100000000) the space 26844K, 59% used [0x00000000acaa0000, 0x00000000ada5a500, 0x00000000ada5a600, 0x00000000ae4d7000) Metaspace used 20472K, capacity 21143K, committed 21296K, reserved 1069056K class space used 2318K, capacity 2605K, committed 2688K, reserved 1048576K } Event: 4.982 GC heap before {Heap before GC invocations=12 (full 1): def new generation total 12096K, used 10752K [0x0000000083000000, 0x0000000083d20000, 0x00000000acaa0000) eden space 10752K, 100% used [0x0000000083000000, 0x0000000083a80000, 0x0000000083a80000) from space 1344K, 0% used [0x0000000083a80000, 0x0000000083a80000, 0x0000000083bd0000) to space 1344K, 0% used [0x0000000083bd0000, 0x0000000083bd0000, 0x0000000083d20000) tenured generation total 26844K, used 16105K [0x00000000acaa0000, 0x00000000ae4d7000, 0x0000000100000000) the space 26844K, 59% used [0x00000000acaa0000, 0x00000000ada5a500, 0x00000000ada5a600, 0x00000000ae4d7000) Metaspace used 22503K, capacity 23266K, committed 23600K, reserved 1071104K class space used 2542K, capacity 2842K, committed 2944K, reserved 1048576K } Event: 4.986 GC heap after {Heap after GC invocations=13 (full 1): def new generation total 12096K, used 604K [0x0000000083000000, 0x0000000083d20000, 0x00000000acaa0000) eden space 10752K, 0% used [0x0000000083000000, 0x0000000083000000, 0x0000000083a80000) from space 1344K, 44% used [0x0000000083bd0000, 0x0000000083c67048, 0x0000000083d20000) to space 1344K, 0% used [0x0000000083a80000, 0x0000000083a80000, 0x0000000083bd0000) tenured generation total 26844K, used 18085K [0x00000000acaa0000, 0x00000000ae4d7000, 0x0000000100000000) the space 26844K, 67% used [0x00000000acaa0000, 0x00000000adc49528, 0x00000000adc49600, 0x00000000ae4d7000) Metaspace used 22503K, capacity 23266K, committed 23600K, reserved 1071104K class space used 2542K, capacity 2842K, committed 2944K, reserved 1048576K } Deoptimization events (20 events): Event: 5.490 Thread 0x00007f2bd0017000 Uncommon trap: trap_request=0xffffffde fr.pc=0x00007f2bc0454f44 relative=0x0000000000000124 Event: 5.490 Thread 0x00007f2bd0017000 Uncommon trap: reason=class_check action=maybe_recompile pc=0x00007f2bc0454f44 method=jdk.internal.misc.Unsafe.allocateUninitializedArray(Ljava/lang/Class;I)Ljava/lang/Object; @ 48 c2 Event: 5.490 Thread 0x00007f2bd0017000 DEOPT PACKING pc=0x00007f2bc0454f44 sp=0x00007f2bd6511d40 Event: 5.490 Thread 0x00007f2bd0017000 DEOPT UNPACKING pc=0x00007f2bb889cea5 sp=0x00007f2bd6511ce8 mode 2 Event: 5.490 Thread 0x00007f2bd0017000 Uncommon trap: trap_request=0xffffffde fr.pc=0x00007f2bc0454f44 relative=0x0000000000000124 Event: 5.490 Thread 0x00007f2bd0017000 Uncommon trap: reason=class_check action=maybe_recompile pc=0x00007f2bc0454f44 method=jdk.internal.misc.Unsafe.allocateUninitializedArray(Ljava/lang/Class;I)Ljava/lang/Object; @ 48 c2 Event: 5.490 Thread 0x00007f2bd0017000 DEOPT PACKING pc=0x00007f2bc0454f44 sp=0x00007f2bd6511d40 Event: 5.490 Thread 0x00007f2bd0017000 DEOPT UNPACKING pc=0x00007f2bb889cea5 sp=0x00007f2bd6511ce8 mode 2 Event: 5.490 Thread 0x00007f2bd0017000 Uncommon trap: trap_request=0xffffffde fr.pc=0x00007f2bc0454f44 relative=0x0000000000000124 Event: 5.490 Thread 0x00007f2bd0017000 Uncommon trap: reason=class_check action=maybe_recompile pc=0x00007f2bc0454f44 method=jdk.internal.misc.Unsafe.allocateUninitializedArray(Ljava/lang/Class;I)Ljava/lang/Object; @ 48 c2 Event: 5.490 Thread 0x00007f2bd0017000 DEOPT PACKING pc=0x00007f2bc0454f44 sp=0x00007f2bd6511d40 Event: 5.490 Thread 0x00007f2bd0017000 DEOPT UNPACKING pc=0x00007f2bb889cea5 sp=0x00007f2bd6511ce8 mode 2 Event: 5.612 Thread 0x00007f2bd0017000 Uncommon trap: trap_request=0xffffffde fr.pc=0x00007f2bc03e2860 relative=0x00000000000000a0 Event: 5.612 Thread 0x00007f2bd0017000 Uncommon trap: reason=class_check action=maybe_recompile pc=0x00007f2bc03e2860 method=com.google.common.collect.TransformedIterator.next()Ljava/lang/Object; @ 10 c2 Event: 5.612 Thread 0x00007f2bd0017000 DEOPT PACKING pc=0x00007f2bc03e2860 sp=0x00007f2bd6511b10 Event: 5.612 Thread 0x00007f2bd0017000 DEOPT UNPACKING pc=0x00007f2bb889cea5 sp=0x00007f2bd6511ac0 mode 2 Event: 5.612 Thread 0x00007f2bd0017000 Uncommon trap: trap_request=0xffffffde fr.pc=0x00007f2bc03e2860 relative=0x00000000000000a0 Event: 5.612 Thread 0x00007f2bd0017000 Uncommon trap: reason=class_check action=maybe_recompile pc=0x00007f2bc03e2860 method=com.google.common.collect.TransformedIterator.next()Ljava/lang/Object; @ 10 c2 Event: 5.612 Thread 0x00007f2bd0017000 DEOPT PACKING pc=0x00007f2bc03e2860 sp=0x00007f2bd6511b40 Event: 5.612 Thread 0x00007f2bd0017000 DEOPT UNPACKING pc=0x00007f2bb889cea5 sp=0x00007f2bd6511af0 mode 2 Classes redefined (0 events): No events Internal exceptions (20 events): Event: 3.486 Thread 0x00007f2bd0017000 Exception (0x000000008356fdb0) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 772] Event: 3.486 Thread 0x00007f2bd0017000 Exception (0x0000000083573d88) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 772] Event: 3.596 Thread 0x00007f2bd0017000 Exception (0x000000008378f598) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 772] Event: 3.614 Thread 0x00007f2bd0017000 Exception (0x00000000837fd290) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 772] Event: 3.621 Thread 0x00007f2bd0017000 Exception (0x00000000838116e0) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 772] Event: 3.621 Thread 0x00007f2bd0017000 Exception (0x00000000838143c0) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 839] Event: 3.691 Thread 0x00007f2bd0017000 Exception (0x0000000083a00f70) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 772] Event: 4.202 Thread 0x00007f2bd0017000 Exception (0x00000000833c3948) thrown at [src/hotspot/share/classfile/systemDictionary.cpp, line 231] Event: 4.327 Thread 0x00007f2bd0017000 Exception (0x00000000835d4428) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 772] Event: 4.329 Thread 0x00007f2bd0017000 Exception (0x0000000083607cf8) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 772] Event: 4.502 Thread 0x00007f2bd0017000 Exception (0x000000008311f8a0) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 772] Event: 4.610 Thread 0x00007f2bd0017000 Exception (0x000000008350c618) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 772] Event: 4.610 Thread 0x00007f2bd0017000 Exception (0x000000008350f9d0) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 772] Event: 4.611 Thread 0x00007f2bd0017000 Exception (0x00000000835349b0) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 772] Event: 4.834 Thread 0x00007f2bd0017000 Exception (0x00000000835d8a28) thrown at [src/hotspot/share/classfile/systemDictionary.cpp, line 231] Event: 4.837 Thread 0x00007f2bd0017000 Exception (0x000000008361a6c8) thrown at [src/hotspot/share/prims/jni.cpp, line 616] Event: 4.881 Thread 0x00007f2bd0017000 Exception (0x0000000083754cb0) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 772] Event: 4.902 Thread 0x00007f2bd0017000 Exception (0x00000000837d9310) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 839] Event: 4.920 Thread 0x00007f2bd0017000 Implicit null exception at 0x00007f2bc041106c to 0x00007f2bc0411114 Event: 5.035 Thread 0x00007f2bd0017000 Exception (0x0000000083070f38) thrown at [src/hotspot/share/interpreter/linkResolver.cpp, line 772] Events (20 events): Event: 5.612 loading class org/sosy_lab/java_smt/api/Formula done Event: 5.612 loading class org/sosy_lab/java_smt/basicimpl/AbstractQuantifiedFormulaManager Event: 5.612 loading class org/sosy_lab/java_smt/basicimpl/AbstractQuantifiedFormulaManager done Event: 5.612 Protecting memory [0x00007f2bd7d96000,0x00007f2bd7d97000] with protection modes 1 Event: 26.721 Loaded shared library /usr/lib/jvm/java-11-openjdk-amd64/lib/server/libjvm.so Event: 61.540 Executing VM operation: RevokeBias Event: 61.540 Executing VM operation: RevokeBias done Event: 61.540 loading class com/google/common/collect/MapMakerInternalMap$KeyIterator Event: 61.540 loading class com/google/common/collect/MapMakerInternalMap$KeyIterator done Event: 61.540 loading class com/google/common/collect/MapMakerInternalMap$HashIterator Event: 61.540 loading class com/google/common/collect/MapMakerInternalMap$HashIterator done Event: 61.540 loading class com/google/common/collect/MapMakerInternalMap$WriteThroughEntry Event: 61.540 loading class com/google/common/collect/MapMakerInternalMap$WriteThroughEntry done Event: 61.541 Executing VM operation: RevokeBias Event: 61.541 Executing VM operation: RevokeBias done Event: 61.541 Executing VM operation: RevokeBias Event: 61.541 Executing VM operation: RevokeBias done Event: 61.561 Thread 0x00007f2b90004000 Thread added: 0x00007f2b90004000 Event: 61.562 Thread 0x00007f2bd04a7800 Thread exited: 0x00007f2bd04a7800 Event: 61.562 Protecting memory [0x00007f2b89ea5000,0x00007f2b89ea9000] with protection modes 0 Dynamic libraries: 83000000-83d20000 rw-p 00000000 00:00 0 83d20000-acaa0000 ---p 00000000 00:00 0 acaa0000-ae4d7000 rw-p 00000000 00:00 0 ae4d7000-100000000 ---p 00000000 00:00 0 800000000-800002000 rwxp 00001000 08:01 132232 /usr/lib/jvm/java-11-openjdk-amd64/lib/server/classes.jsa 800002000-8003b7000 rw-p 00003000 08:01 132232 /usr/lib/jvm/java-11-openjdk-amd64/lib/server/classes.jsa 8003b7000-800a97000 r--p 003b8000 08:01 132232 /usr/lib/jvm/java-11-openjdk-amd64/lib/server/classes.jsa 800a97000-800a98000 rw-p 00a98000 08:01 132232 /usr/lib/jvm/java-11-openjdk-amd64/lib/server/classes.jsa 800a98000-8010a8000 r--p 00a99000 08:01 132232 /usr/lib/jvm/java-11-openjdk-amd64/lib/server/classes.jsa 840000000-8402e0000 rw-p 00000000 00:00 0 8402e0000-880000000 ---p 00000000 00:00 0 55b814fad000-55b814fae000 r--p 00000000 08:01 133765 /usr/lib/jvm/java-11-openjdk-amd64/bin/java 55b814fae000-55b814faf000 r-xp 00001000 08:01 133765 /usr/lib/jvm/java-11-openjdk-amd64/bin/java 55b814faf000-55b814fb0000 r--p 00002000 08:01 133765 /usr/lib/jvm/java-11-openjdk-amd64/bin/java 55b814fb0000-55b814fb1000 r--p 00002000 08:01 133765 /usr/lib/jvm/java-11-openjdk-amd64/bin/java 55b814fb1000-55b814fb2000 rw-p 00003000 08:01 133765 /usr/lib/jvm/java-11-openjdk-amd64/bin/java 55b81601f000-55b816060000 rw-p 00000000 00:00 0 [heap] 7f2b7c000000-7f2b7d579000 rw-p 00000000 00:00 0 7f2b7d579000-7f2b80000000 ---p 00000000 00:00 0 7f2b80000000-7f2b80021000 rw-p 00000000 00:00 0 7f2b80021000-7f2b84000000 ---p 00000000 00:00 0 7f2b84000000-7f2b84021000 rw-p 00000000 00:00 0 7f2b84021000-7f2b88000000 ---p 00000000 00:00 0 7f2b88ce2000-7f2b896e3000 rw-p 00000000 00:00 0 7f2b89ea5000-7f2b89ea9000 ---p 00000000 00:00 0 7f2b89ea9000-7f2b8a066000 rw-p 00000000 00:00 0 7f2b8a066000-7f2b8a1a6000 ---p 00000000 00:00 0 7f2b8a1a6000-7f2b8a1d2000 r--p 00000000 08:01 134831 /usr/lib/jvm/java-11-openjdk-amd64/lib/libawt.so 7f2b8a1d2000-7f2b8a23b000 r-xp 0002c000 08:01 134831 /usr/lib/jvm/java-11-openjdk-amd64/lib/libawt.so 7f2b8a23b000-7f2b8a247000 r--p 00095000 08:01 134831 /usr/lib/jvm/java-11-openjdk-amd64/lib/libawt.so 7f2b8a247000-7f2b8a248000 ---p 000a1000 08:01 134831 /usr/lib/jvm/java-11-openjdk-amd64/lib/libawt.so 7f2b8a248000-7f2b8a249000 r--p 000a1000 08:01 134831 /usr/lib/jvm/java-11-openjdk-amd64/lib/libawt.so 7f2b8a249000-7f2b8a254000 rw-p 000a2000 08:01 134831 /usr/lib/jvm/java-11-openjdk-amd64/lib/libawt.so 7f2b8a254000-7f2b8a465000 rw-p 00000000 00:00 0 7f2b8a465000-7f2b8a479000 ---p 00000000 00:00 0 7f2b8a479000-7f2b8a4a5000 r-xp 00000000 00:325 1266346 /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/libz3java.so 7f2b8a4a5000-7f2b8a6a4000 ---p 0002c000 00:325 1266346 /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/libz3java.so 7f2b8a6a4000-7f2b8a6a5000 r--p 0002b000 00:325 1266346 /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/libz3java.so 7f2b8a6a5000-7f2b8a6a7000 rw-p 0002c000 00:325 1266346 /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/libz3java.so 7f2b8a6a7000-7f2b8bdd5000 r-xp 00000000 00:325 1266345 /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/libz3.so 7f2b8bdd5000-7f2b8bfd5000 ---p 0172e000 00:325 1266345 /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/libz3.so 7f2b8bfd5000-7f2b8bffc000 r--p 0172e000 00:325 1266345 /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/libz3.so 7f2b8bffc000-7f2b8bfff000 rw-p 01755000 00:325 1266345 /tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/libz3.so 7f2b8bfff000-7f2b8c000000 rw-p 00000000 00:00 0 7f2b8c000000-7f2b8c021000 rw-p 00000000 00:00 0 7f2b8c021000-7f2b90000000 ---p 00000000 00:00 0 7f2b90000000-7f2b90021000 rw-p 00000000 00:00 0 7f2b90021000-7f2b94000000 ---p 00000000 00:00 0 7f2b94000000-7f2b94021000 rw-p 00000000 00:00 0 7f2b94021000-7f2b98000000 ---p 00000000 00:00 0 7f2b98000000-7f2b98021000 rw-p 00000000 00:00 0 7f2b98021000-7f2b9c000000 ---p 00000000 00:00 0 7f2b9c000000-7f2b9c629000 rw-p 00000000 00:00 0 7f2b9c629000-7f2ba0000000 ---p 00000000 00:00 0 7f2ba0000000-7f2ba05cf000 rw-p 00000000 00:00 0 7f2ba05cf000-7f2ba4000000 ---p 00000000 00:00 0 7f2ba4000000-7f2ba4021000 rw-p 00000000 00:00 0 7f2ba4021000-7f2ba8000000 ---p 00000000 00:00 0 7f2ba8000000-7f2ba8021000 rw-p 00000000 00:00 0 7f2ba8021000-7f2bac000000 ---p 00000000 00:00 0 7f2bac000000-7f2bac021000 rw-p 00000000 00:00 0 7f2bac021000-7f2bb0000000 ---p 00000000 00:00 0 7f2bb0000000-7f2bb0021000 rw-p 00000000 00:00 0 7f2bb0021000-7f2bb4000000 ---p 00000000 00:00 0 7f2bb4000000-7f2bb4023000 rw-p 00000000 00:00 0 7f2bb4023000-7f2bb8000000 ---p 00000000 00:00 0 7f2bb8053000-7f2bb8253000 rw-p 00000000 00:00 0 7f2bb8253000-7f2bb8453000 rw-p 00000000 00:00 0 7f2bb8453000-7f2bb8653000 rw-p 00000000 00:00 0 7f2bb8653000-7f2bb8853000 rw-p 00000000 00:00 0 7f2bb8853000-7f2bb8ac3000 rwxp 00000000 00:00 0 7f2bb8ac3000-7f2bb8de2000 ---p 00000000 00:00 0 7f2bb8de2000-7f2bb9642000 rwxp 00000000 00:00 0 7f2bb9642000-7f2bc031a000 ---p 00000000 00:00 0 7f2bc031a000-7f2bc058a000 rwxp 00000000 00:00 0 7f2bc058a000-7f2bc7853000 ---p 00000000 00:00 0 7f2bc7853000-7f2bd0000000 r--s 00000000 08:01 135462 /usr/lib/jvm/java-11-openjdk-amd64/lib/modules 7f2bd0000000-7f2bd4000000 rw-p 00000000 00:00 0 7f2bd4084000-7f2bd4087000 r--p 00000000 08:01 134833 /usr/lib/jvm/java-11-openjdk-amd64/lib/libawt_headless.so 7f2bd4087000-7f2bd408b000 r-xp 00003000 08:01 134833 /usr/lib/jvm/java-11-openjdk-amd64/lib/libawt_headless.so 7f2bd408b000-7f2bd408d000 r--p 00007000 08:01 134833 /usr/lib/jvm/java-11-openjdk-amd64/lib/libawt_headless.so 7f2bd408d000-7f2bd408e000 r--p 00008000 08:01 134833 /usr/lib/jvm/java-11-openjdk-amd64/lib/libawt_headless.so 7f2bd408e000-7f2bd408f000 rw-p 00009000 08:01 134833 /usr/lib/jvm/java-11-openjdk-amd64/lib/libawt_headless.so 7f2bd408f000-7f2bd428f000 rw-p 00000000 00:00 0 7f2bd428f000-7f2bd4293000 ---p 00000000 00:00 0 7f2bd4293000-7f2bd4390000 rw-p 00000000 00:00 0 7f2bd4390000-7f2bd4394000 ---p 00000000 00:00 0 7f2bd4394000-7f2bd4491000 rw-p 00000000 00:00 0 7f2bd4491000-7f2bd4493000 r--p 00000000 08:01 134880 /usr/lib/jvm/java-11-openjdk-amd64/lib/libmanagement_ext.so 7f2bd4493000-7f2bd4496000 r-xp 00002000 08:01 134880 /usr/lib/jvm/java-11-openjdk-amd64/lib/libmanagement_ext.so 7f2bd4496000-7f2bd4498000 r--p 00005000 08:01 134880 /usr/lib/jvm/java-11-openjdk-amd64/lib/libmanagement_ext.so 7f2bd4498000-7f2bd4499000 r--p 00006000 08:01 134880 /usr/lib/jvm/java-11-openjdk-amd64/lib/libmanagement_ext.so 7f2bd4499000-7f2bd449a000 rw-p 00007000 08:01 134880 /usr/lib/jvm/java-11-openjdk-amd64/lib/libmanagement_ext.so 7f2bd449a000-7f2bd44cb000 rw-p 00000000 00:00 0 7f2bd44cb000-7f2bd44cf000 r--p 00000000 08:01 135357 /usr/lib/jvm/java-11-openjdk-amd64/lib/libnet.so 7f2bd44cf000-7f2bd44de000 r-xp 00004000 08:01 135357 /usr/lib/jvm/java-11-openjdk-amd64/lib/libnet.so 7f2bd44de000-7f2bd44e2000 r--p 00013000 08:01 135357 /usr/lib/jvm/java-11-openjdk-amd64/lib/libnet.so 7f2bd44e2000-7f2bd44e3000 r--p 00016000 08:01 135357 /usr/lib/jvm/java-11-openjdk-amd64/lib/libnet.so 7f2bd44e3000-7f2bd44e4000 rw-p 00017000 08:01 135357 /usr/lib/jvm/java-11-openjdk-amd64/lib/libnet.so 7f2bd44e4000-7f2bd44eb000 r--p 00000000 08:01 135452 /usr/lib/jvm/java-11-openjdk-amd64/lib/libnio.so 7f2bd44eb000-7f2bd44f3000 r-xp 00007000 08:01 135452 /usr/lib/jvm/java-11-openjdk-amd64/lib/libnio.so 7f2bd44f3000-7f2bd44f6000 r--p 0000f000 08:01 135452 /usr/lib/jvm/java-11-openjdk-amd64/lib/libnio.so 7f2bd44f6000-7f2bd44f7000 r--p 00011000 08:01 135452 /usr/lib/jvm/java-11-openjdk-amd64/lib/libnio.so 7f2bd44f7000-7f2bd44f8000 rw-p 00012000 08:01 135452 /usr/lib/jvm/java-11-openjdk-amd64/lib/libnio.so 7f2bd44f8000-7f2bd44fc000 ---p 00000000 00:00 0 7f2bd44fc000-7f2bd45f9000 rw-p 00000000 00:00 0 7f2bd45f9000-7f2bd45fa000 ---p 00000000 00:00 0 7f2bd45fa000-7f2bd46fb000 rw-p 00000000 00:00 0 7f2bd46fb000-7f2bd46ff000 ---p 00000000 00:00 0 7f2bd46ff000-7f2bd47fc000 rw-p 00000000 00:00 0 7f2bd47fc000-7f2bd4800000 ---p 00000000 00:00 0 7f2bd4800000-7f2bd48fd000 rw-p 00000000 00:00 0 7f2bd48fd000-7f2bd4901000 ---p 00000000 00:00 0 7f2bd4901000-7f2bd49fe000 rw-p 00000000 00:00 0 7f2bd49fe000-7f2bd4a02000 ---p 00000000 00:00 0 7f2bd4a02000-7f2bd4aff000 rw-p 00000000 00:00 0 7f2bd4aff000-7f2bd4b03000 ---p 00000000 00:00 0 7f2bd4b03000-7f2bd4c00000 rw-p 00000000 00:00 0 7f2bd4c00000-7f2bd4c03000 r--p 00000000 08:01 10898 /usr/lib/x86_64-linux-gnu/libnss_files-2.31.so 7f2bd4c03000-7f2bd4c0a000 r-xp 00003000 08:01 10898 /usr/lib/x86_64-linux-gnu/libnss_files-2.31.so 7f2bd4c0a000-7f2bd4c0c000 r--p 0000a000 08:01 10898 /usr/lib/x86_64-linux-gnu/libnss_files-2.31.so 7f2bd4c0c000-7f2bd4c0d000 r--p 0000b000 08:01 10898 /usr/lib/x86_64-linux-gnu/libnss_files-2.31.so 7f2bd4c0d000-7f2bd4c0e000 rw-p 0000c000 08:01 10898 /usr/lib/x86_64-linux-gnu/libnss_files-2.31.so 7f2bd4c0e000-7f2bd4c14000 rw-p 00000000 00:00 0 7f2bd4c17000-7f2bd4c1a000 r--p 00000000 08:01 134876 /usr/lib/jvm/java-11-openjdk-amd64/lib/libmanagement.so 7f2bd4c1a000-7f2bd4c1b000 r-xp 00003000 08:01 134876 /usr/lib/jvm/java-11-openjdk-amd64/lib/libmanagement.so 7f2bd4c1b000-7f2bd4c1c000 r--p 00004000 08:01 134876 /usr/lib/jvm/java-11-openjdk-amd64/lib/libmanagement.so 7f2bd4c1c000-7f2bd4c1d000 r--p 00004000 08:01 134876 /usr/lib/jvm/java-11-openjdk-amd64/lib/libmanagement.so 7f2bd4c1d000-7f2bd4c1e000 rw-p 00005000 08:01 134876 /usr/lib/jvm/java-11-openjdk-amd64/lib/libmanagement.so 7f2bd4c1e000-7f2bd4f04000 r--p 00000000 08:01 1387 /usr/lib/locale/locale-archive 7f2bd4f04000-7f2bd4f08000 ---p 00000000 00:00 0 7f2bd4f08000-7f2bd5005000 rw-p 00000000 00:00 0 7f2bd5005000-7f2bd5009000 ---p 00000000 00:00 0 7f2bd5009000-7f2bd5106000 rw-p 00000000 00:00 0 7f2bd5106000-7f2bd5107000 ---p 00000000 00:00 0 7f2bd5107000-7f2bd5b0c000 rw-p 00000000 00:00 0 7f2bd5b0c000-7f2bd5b5c000 rw-p 00000000 00:00 0 7f2bd5b5c000-7f2bd5de9000 ---p 00000000 00:00 0 7f2bd5de9000-7f2bd5df0000 rw-p 00000000 00:00 0 7f2bd5df0000-7f2bd5f36000 ---p 00000000 00:00 0 7f2bd5f36000-7f2bd5f44000 rw-p 00000000 00:00 0 7f2bd5f44000-7f2bd61d1000 ---p 00000000 00:00 0 7f2bd61d1000-7f2bd61d7000 rw-p 00000000 00:00 0 7f2bd61d7000-7f2bd62bd000 ---p 00000000 00:00 0 7f2bd62bd000-7f2bd62ce000 rw-p 00000000 00:00 0 7f2bd62ce000-7f2bd63a8000 ---p 00000000 00:00 0 7f2bd63a8000-7f2bd63ad000 rw-p 00000000 00:00 0 7f2bd63ad000-7f2bd63b4000 ---p 00000000 00:00 0 7f2bd63b4000-7f2bd63b6000 r--p 00000000 08:01 135461 /usr/lib/jvm/java-11-openjdk-amd64/lib/libzip.so 7f2bd63b6000-7f2bd63ba000 r-xp 00002000 08:01 135461 /usr/lib/jvm/java-11-openjdk-amd64/lib/libzip.so 7f2bd63ba000-7f2bd63bc000 r--p 00006000 08:01 135461 /usr/lib/jvm/java-11-openjdk-amd64/lib/libzip.so 7f2bd63bc000-7f2bd63bd000 r--p 00007000 08:01 135461 /usr/lib/jvm/java-11-openjdk-amd64/lib/libzip.so 7f2bd63bd000-7f2bd63be000 rw-p 00008000 08:01 135461 /usr/lib/jvm/java-11-openjdk-amd64/lib/libzip.so 7f2bd63be000-7f2bd63c6000 rw-p 00000000 00:00 0 7f2bd63c6000-7f2bd63c7000 ---p 00000000 00:00 0 7f2bd63c7000-7f2bd63c8000 r--p 00000000 00:00 0 7f2bd63c8000-7f2bd63d6000 r--p 00000000 08:01 134862 /usr/lib/jvm/java-11-openjdk-amd64/lib/libjava.so 7f2bd63d6000-7f2bd63ec000 r-xp 0000e000 08:01 134862 /usr/lib/jvm/java-11-openjdk-amd64/lib/libjava.so 7f2bd63ec000-7f2bd63f3000 r--p 00024000 08:01 134862 /usr/lib/jvm/java-11-openjdk-amd64/lib/libjava.so 7f2bd63f3000-7f2bd63f4000 r--p 0002a000 08:01 134862 /usr/lib/jvm/java-11-openjdk-amd64/lib/libjava.so 7f2bd63f4000-7f2bd63f5000 rw-p 0002b000 08:01 134862 /usr/lib/jvm/java-11-openjdk-amd64/lib/libjava.so 7f2bd63f5000-7f2bd63f6000 rw-p 00000000 00:00 0 7f2bd63f6000-7f2bd63fb000 r--p 00000000 08:01 135460 /usr/lib/jvm/java-11-openjdk-amd64/lib/libverify.so 7f2bd63fb000-7f2bd6402000 r-xp 00005000 08:01 135460 /usr/lib/jvm/java-11-openjdk-amd64/lib/libverify.so 7f2bd6402000-7f2bd6404000 r--p 0000c000 08:01 135460 /usr/lib/jvm/java-11-openjdk-amd64/lib/libverify.so 7f2bd6404000-7f2bd6405000 ---p 0000e000 08:01 135460 /usr/lib/jvm/java-11-openjdk-amd64/lib/libverify.so 7f2bd6405000-7f2bd6407000 r--p 0000e000 08:01 135460 /usr/lib/jvm/java-11-openjdk-amd64/lib/libverify.so 7f2bd6407000-7f2bd6408000 rw-p 00010000 08:01 135460 /usr/lib/jvm/java-11-openjdk-amd64/lib/libverify.so 7f2bd6408000-7f2bd640b000 r--p 00000000 08:01 10953 /usr/lib/x86_64-linux-gnu/librt-2.31.so 7f2bd640b000-7f2bd640f000 r-xp 00003000 08:01 10953 /usr/lib/x86_64-linux-gnu/librt-2.31.so 7f2bd640f000-7f2bd6410000 r--p 00007000 08:01 10953 /usr/lib/x86_64-linux-gnu/librt-2.31.so 7f2bd6410000-7f2bd6411000 ---p 00008000 08:01 10953 /usr/lib/x86_64-linux-gnu/librt-2.31.so 7f2bd6411000-7f2bd6412000 r--p 00008000 08:01 10953 /usr/lib/x86_64-linux-gnu/librt-2.31.so 7f2bd6412000-7f2bd6413000 rw-p 00009000 08:01 10953 /usr/lib/x86_64-linux-gnu/librt-2.31.so 7f2bd6413000-7f2bd6417000 ---p 00000000 00:00 0 7f2bd6417000-7f2bd6514000 rw-p 00000000 00:00 0 7f2bd6514000-7f2bd6517000 r--p 00000000 08:01 18431 /usr/lib/x86_64-linux-gnu/libgcc_s.so.1 7f2bd6517000-7f2bd6529000 r-xp 00003000 08:01 18431 /usr/lib/x86_64-linux-gnu/libgcc_s.so.1 7f2bd6529000-7f2bd652d000 r--p 00015000 08:01 18431 /usr/lib/x86_64-linux-gnu/libgcc_s.so.1 7f2bd652d000-7f2bd652e000 r--p 00018000 08:01 18431 /usr/lib/x86_64-linux-gnu/libgcc_s.so.1 7f2bd652e000-7f2bd652f000 rw-p 00019000 08:01 18431 /usr/lib/x86_64-linux-gnu/libgcc_s.so.1 7f2bd652f000-7f2bd653e000 r--p 00000000 08:01 10885 /usr/lib/x86_64-linux-gnu/libm-2.31.so 7f2bd653e000-7f2bd65e5000 r-xp 0000f000 08:01 10885 /usr/lib/x86_64-linux-gnu/libm-2.31.so 7f2bd65e5000-7f2bd667c000 r--p 000b6000 08:01 10885 /usr/lib/x86_64-linux-gnu/libm-2.31.so 7f2bd667c000-7f2bd667d000 r--p 0014c000 08:01 10885 /usr/lib/x86_64-linux-gnu/libm-2.31.so 7f2bd667d000-7f2bd667e000 rw-p 0014d000 08:01 10885 /usr/lib/x86_64-linux-gnu/libm-2.31.so 7f2bd667e000-7f2bd6714000 r--p 00000000 08:01 3827 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.28 7f2bd6714000-7f2bd6805000 r-xp 00096000 08:01 3827 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.28 7f2bd6805000-7f2bd684e000 r--p 00187000 08:01 3827 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.28 7f2bd684e000-7f2bd684f000 ---p 001d0000 08:01 3827 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.28 7f2bd684f000-7f2bd685a000 r--p 001d0000 08:01 3827 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.28 7f2bd685a000-7f2bd685d000 rw-p 001db000 08:01 3827 /usr/lib/x86_64-linux-gnu/libstdc++.so.6.0.28 7f2bd685d000-7f2bd6860000 rw-p 00000000 00:00 0 7f2bd6860000-7f2bd6ae1000 r--p 00000000 08:01 135465 /usr/lib/jvm/java-11-openjdk-amd64/lib/server/libjvm.so 7f2bd6ae1000-7f2bd7761000 r-xp 00281000 08:01 135465 /usr/lib/jvm/java-11-openjdk-amd64/lib/server/libjvm.so 7f2bd7761000-7f2bd79bc000 r--p 00f01000 08:01 135465 /usr/lib/jvm/java-11-openjdk-amd64/lib/server/libjvm.so 7f2bd79bc000-7f2bd7a80000 r--p 0115b000 08:01 135465 /usr/lib/jvm/java-11-openjdk-amd64/lib/server/libjvm.so 7f2bd7a80000-7f2bd7abb000 rw-p 0121f000 08:01 135465 /usr/lib/jvm/java-11-openjdk-amd64/lib/server/libjvm.so 7f2bd7abb000-7f2bd7b14000 rw-p 00000000 00:00 0 7f2bd7b14000-7f2bd7b1b000 r--p 00000000 08:01 10920 /usr/lib/x86_64-linux-gnu/libpthread-2.31.so 7f2bd7b1b000-7f2bd7b2c000 r-xp 00007000 08:01 10920 /usr/lib/x86_64-linux-gnu/libpthread-2.31.so 7f2bd7b2c000-7f2bd7b31000 r--p 00018000 08:01 10920 /usr/lib/x86_64-linux-gnu/libpthread-2.31.so 7f2bd7b31000-7f2bd7b32000 r--p 0001c000 08:01 10920 /usr/lib/x86_64-linux-gnu/libpthread-2.31.so 7f2bd7b32000-7f2bd7b33000 rw-p 0001d000 08:01 10920 /usr/lib/x86_64-linux-gnu/libpthread-2.31.so 7f2bd7b33000-7f2bd7b37000 rw-p 00000000 00:00 0 7f2bd7b37000-7f2bd7b38000 r--p 00000000 08:01 10884 /usr/lib/x86_64-linux-gnu/libdl-2.31.so 7f2bd7b38000-7f2bd7b3a000 r-xp 00001000 08:01 10884 /usr/lib/x86_64-linux-gnu/libdl-2.31.so 7f2bd7b3a000-7f2bd7b3b000 r--p 00003000 08:01 10884 /usr/lib/x86_64-linux-gnu/libdl-2.31.so 7f2bd7b3b000-7f2bd7b3c000 r--p 00003000 08:01 10884 /usr/lib/x86_64-linux-gnu/libdl-2.31.so 7f2bd7b3c000-7f2bd7b3d000 rw-p 00004000 08:01 10884 /usr/lib/x86_64-linux-gnu/libdl-2.31.so 7f2bd7b3d000-7f2bd7b3f000 r--p 00000000 08:01 400 /usr/lib/x86_64-linux-gnu/libz.so.1.2.11 7f2bd7b3f000-7f2bd7b50000 r-xp 00002000 08:01 400 /usr/lib/x86_64-linux-gnu/libz.so.1.2.11 7f2bd7b50000-7f2bd7b56000 r--p 00013000 08:01 400 /usr/lib/x86_64-linux-gnu/libz.so.1.2.11 7f2bd7b56000-7f2bd7b57000 ---p 00019000 08:01 400 /usr/lib/x86_64-linux-gnu/libz.so.1.2.11 7f2bd7b57000-7f2bd7b58000 r--p 00019000 08:01 400 /usr/lib/x86_64-linux-gnu/libz.so.1.2.11 7f2bd7b58000-7f2bd7b59000 rw-p 0001a000 08:01 400 /usr/lib/x86_64-linux-gnu/libz.so.1.2.11 7f2bd7b59000-7f2bd7b7e000 r--p 00000000 08:01 10883 /usr/lib/x86_64-linux-gnu/libc-2.31.so 7f2bd7b7e000-7f2bd7cf6000 r-xp 00025000 08:01 10883 /usr/lib/x86_64-linux-gnu/libc-2.31.so 7f2bd7cf6000-7f2bd7d40000 r--p 0019d000 08:01 10883 /usr/lib/x86_64-linux-gnu/libc-2.31.so 7f2bd7d40000-7f2bd7d41000 ---p 001e7000 08:01 10883 /usr/lib/x86_64-linux-gnu/libc-2.31.so 7f2bd7d41000-7f2bd7d44000 r--p 001e7000 08:01 10883 /usr/lib/x86_64-linux-gnu/libc-2.31.so 7f2bd7d44000-7f2bd7d47000 rw-p 001ea000 08:01 10883 /usr/lib/x86_64-linux-gnu/libc-2.31.so 7f2bd7d47000-7f2bd7d4b000 rw-p 00000000 00:00 0 7f2bd7d4c000-7f2bd7d4e000 r--p 00000000 08:01 134868 /usr/lib/jvm/java-11-openjdk-amd64/lib/libjimage.so 7f2bd7d4e000-7f2bd7d51000 r-xp 00002000 08:01 134868 /usr/lib/jvm/java-11-openjdk-amd64/lib/libjimage.so 7f2bd7d51000-7f2bd7d52000 r--p 00005000 08:01 134868 /usr/lib/jvm/java-11-openjdk-amd64/lib/libjimage.so 7f2bd7d52000-7f2bd7d53000 ---p 00006000 08:01 134868 /usr/lib/jvm/java-11-openjdk-amd64/lib/libjimage.so 7f2bd7d53000-7f2bd7d54000 r--p 00006000 08:01 134868 /usr/lib/jvm/java-11-openjdk-amd64/lib/libjimage.so 7f2bd7d54000-7f2bd7d55000 rw-p 00007000 08:01 134868 /usr/lib/jvm/java-11-openjdk-amd64/lib/libjimage.so 7f2bd7d55000-7f2bd7d58000 r--p 00000000 08:01 134821 /usr/lib/jvm/java-11-openjdk-amd64/lib/jli/libjli.so 7f2bd7d58000-7f2bd7d62000 r-xp 00003000 08:01 134821 /usr/lib/jvm/java-11-openjdk-amd64/lib/jli/libjli.so 7f2bd7d62000-7f2bd7d65000 r--p 0000d000 08:01 134821 /usr/lib/jvm/java-11-openjdk-amd64/lib/jli/libjli.so 7f2bd7d65000-7f2bd7d66000 ---p 00010000 08:01 134821 /usr/lib/jvm/java-11-openjdk-amd64/lib/jli/libjli.so 7f2bd7d66000-7f2bd7d67000 r--p 00010000 08:01 134821 /usr/lib/jvm/java-11-openjdk-amd64/lib/jli/libjli.so 7f2bd7d67000-7f2bd7d68000 rw-p 00011000 08:01 134821 /usr/lib/jvm/java-11-openjdk-amd64/lib/jli/libjli.so 7f2bd7d68000-7f2bd7d6a000 rw-p 00000000 00:00 0 7f2bd7d6a000-7f2bd7d6b000 r--p 00000000 08:01 3851 /usr/lib/x86_64-linux-gnu/ld-2.31.so 7f2bd7d6b000-7f2bd7d8e000 r-xp 00001000 08:01 3851 /usr/lib/x86_64-linux-gnu/ld-2.31.so 7f2bd7d8e000-7f2bd7d96000 r--p 00024000 08:01 3851 /usr/lib/x86_64-linux-gnu/ld-2.31.so 7f2bd7d96000-7f2bd7d97000 r--p 00000000 00:00 0 7f2bd7d97000-7f2bd7d98000 r--p 0002c000 08:01 3851 /usr/lib/x86_64-linux-gnu/ld-2.31.so 7f2bd7d98000-7f2bd7d99000 rw-p 0002d000 08:01 3851 /usr/lib/x86_64-linux-gnu/ld-2.31.so 7f2bd7d99000-7f2bd7d9a000 rw-p 00000000 00:00 0 7ffd46538000-7ffd46559000 rw-p 00000000 00:00 0 [stack] 7ffd4657e000-7ffd46581000 r--p 00000000 00:00 0 [vvar] 7ffd46581000-7ffd46582000 r-xp 00000000 00:00 0 [vdso] ffffffffff600000-ffffffffff601000 --xp 00000000 00:00 0 [vsyscall] VM Arguments: jvm_args: -XX:+PerfDisableSharedMem -Djava.awt.headless=true -Xss1024k -Xmx2000M -ea java_command: org.sosy_lab.cpachecker.cmdline.CPAMain -noout -predicateAnalysis -setprop cpa.predicate.abstraction.computation=ELIMINATION -setprop solver.solver=Z3 -setprop analysis.algorithm.CEGAR=false -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -timelimit 60s -stats -spec test/programs/benchmarks/properties/unreach-call.prp -32 test/programs/benchmarks/seq-mthreaded-reduced/pals_floodmax.3.2.ufo.UNBOUNDED.pals.c.v+nlh-reducer.c java_class_path (initial): :/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/bin:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/cpachecker.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/jsylvan.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/gmp.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/apron.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/jpl.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/org.eclipse.equinox.preferences.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/org.eclipse.equinox.common.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/ultimate-core-rcp.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/java-cup-runtime.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/ultimate-model-checker-utils.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/icu4j.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/batik-ext.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/batik-util.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/javabdd.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/ultimate-core Launcher Type: SUN_STANDARD [Global flags] intx CICompilerCount = 2 {product} {ergonomic} size_t InitialHeapSize = 39845888 {product} {ergonomic} size_t MaxHeapSize = 2097152000 {product} {command line} size_t MaxNewSize = 699006976 {product} {ergonomic} size_t MinHeapDeltaBytes = 196608 {product} {ergonomic} size_t NewSize = 13238272 {product} {ergonomic} uintx NonNMethodCodeHeapSize = 5825164 {pd product} {ergonomic} uintx NonProfiledCodeHeapSize = 122916538 {pd product} {ergonomic} size_t OldSize = 26607616 {product} {ergonomic} bool PerfDisableSharedMem = true {product} {command line} uintx ProfiledCodeHeapSize = 122916538 {pd product} {ergonomic} uintx ReservedCodeCacheSize = 251658240 {pd product} {ergonomic} bool SegmentedCodeCache = true {product} {ergonomic} intx ThreadStackSize = 1024 {pd product} {command line} bool UseCompressedClassPointers = true {lp64_product} {ergonomic} bool UseCompressedOops = true {lp64_product} {ergonomic} bool UseSerialGC = true {product} {ergonomic} Logging: Log output configuration: #0: stdout all=warning uptime,level,tags #1: stderr all=off uptime,level,tags Environment Variables: CLASSPATH=:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/bin:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/cpachecker.jar:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/*:/tmp/vcloud_worker_vcloud-master_on_vcloud-master/run_dir_11dd9b86-56f2-40dd-884c-e0cd0522d308/lib/java/runtime/* PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/usr/local/games:/snap/bin SHELL=/bin/sh LANG=en_US.UTF-8 Signal Handlers: SIGSEGV: [libjvm.so+0xe8e8d0], sa_mask[0]=11111111011111111101111111111110, sa_flags=SA_RESTART|SA_SIGINFO SIGBUS: [libjvm.so+0xe8e8d0], sa_mask[0]=11111111011111111101111111111110, sa_flags=SA_RESTART|SA_SIGINFO SIGFPE: [libjvm.so+0xe8e8d0], sa_mask[0]=11111111011111111101111111111110, sa_flags=SA_RESTART|SA_SIGINFO SIGPIPE: [libjvm.so+0xbd6910], sa_mask[0]=11111111011111111101111111111110, sa_flags=SA_RESTART|SA_SIGINFO SIGXFSZ: [libjvm.so+0xbd6910], sa_mask[0]=11111111011111111101111111111110, sa_flags=SA_RESTART|SA_SIGINFO SIGILL: [libjvm.so+0xe8e8d0], sa_mask[0]=11111111011111111101111111111110, sa_flags=SA_RESTART|SA_SIGINFO SIGUSR2: [libjvm.so+0xbd67b0], sa_mask[0]=00000000000000000000000000000000, sa_flags=SA_RESTART|SA_SIGINFO SIGHUP: SIG_IGN, sa_mask[0]=00000000000000000000000000000000, sa_flags=none SIGINT: [libjvm.so+0xbd6c50], sa_mask[0]=11111111011111111101111111111110, sa_flags=SA_RESTART|SA_SIGINFO SIGTERM: [libjvm.so+0xbd6c50], sa_mask[0]=11111111011111111101111111111110, sa_flags=SA_RESTART|SA_SIGINFO SIGQUIT: [libjvm.so+0xbd6c50], sa_mask[0]=11111111011111111101111111111110, sa_flags=SA_RESTART|SA_SIGINFO --------------- S Y S T E M --------------- OS:DISTRIB_ID=Ubuntu DISTRIB_RELEASE=20.04 DISTRIB_CODENAME=focal DISTRIB_DESCRIPTION="Ubuntu 20.04.3 LTS" uname:Linux 5.4.0-99-generic #112-Ubuntu SMP Thu Feb 3 13:50:55 UTC 2022 x86_64 OS uptime: 1 days 7:02 hours libc:glibc 2.31 NPTL 2.31 rlimit (soft/hard): STACK 8192k/infinity , CORE 0k/infinity , NPROC 127518/127518 , NOFILE 1048576/1048576 , AS infinity/infinity , CPU infinity/infinity , DATA infinity/infinity , FSIZE infinity/infinity , MEMLOCK 65536k/65536k load average:3.55 3.77 3.81 /proc/meminfo: MemTotal: 32702936 kB MemFree: 25610448 kB MemAvailable: 28005888 kB Buffers: 0 kB Cached: 2395440 kB SwapCached: 0 kB Active: 6473304 kB Inactive: 453488 kB Active(anon): 6206904 kB Inactive(anon): 84480 kB Active(file): 266400 kB Inactive(file): 369008 kB Unevictable: 0 kB Mlocked: 0 kB SwapTotal: 0 kB SwapFree: 0 kB Dirty: 528 kB Writeback: 0 kB AnonPages: 4544764 kB Mapped: 47256 kB Shmem: 1746620 kB KReclaimable: 259580 kB Slab: 0 kB SReclaimable: 0 kB SUnreclaim: 0 kB KernelStack: 5584 kB PageTables: 12480 kB NFS_Unstable: 0 kB Bounce: 0 kB WritebackTmp: 0 kB CommitLimit: 16351468 kB Committed_AS: 6992812 kB VmallocTotal: 34359738367 kB VmallocUsed: 16272 kB VmallocChunk: 0 kB Percpu: 36512 kB HardwareCorrupted: 0 kB AnonHugePages: 0 kB ShmemHugePages: 0 kB ShmemPmdMapped: 0 kB FileHugePages: 0 kB FilePmdMapped: 0 kB CmaTotal: 0 kB CmaFree: 0 kB HugePages_Total: 0 HugePages_Free: 0 HugePages_Rsvd: 0 HugePages_Surp: 0 Hugepagesize: 2048 kB Hugetlb: 0 kB DirectMap4k: 368728 kB DirectMap2M: 27760640 kB DirectMap1G: 5242880 kB /sys/kernel/mm/transparent_hugepage/enabled: always [madvise] never /sys/kernel/mm/transparent_hugepage/defrag (defrag/compaction efforts parameter): always defer defer+madvise [madvise] never Process Memory: Virtual Size: 4596920K (peak: 13036584K) Resident Set Size: 218088K (peak: 218088K) (anon: 178524K, file: 39564K, shmem: 0K) Swapped out: 0K C-Heap outstanding allocations: 88376K /proc/sys/kernel/threads-max (system-wide limit on the number of threads): 255036 /proc/sys/vm/max_map_count (maximum number of memory map areas a process may have): 65530 /proc/sys/kernel/pid_max (system-wide limit on number of process identifiers): 4194304 container (cgroup) information: container_type: cgroupv1 cpu_cpuset_cpus: 0 cpu_memory_nodes: 0 active_processor_count: 1 cpu_quota: -1 cpu_period: 100000 cpu_shares: -1 memory_limit_in_bytes: 2499997696 memory_and_swap_limit_in_bytes: 2499997696 memory_soft_limit_in_bytes: -1 memory_usage_in_bytes: 185610240 memory_max_usage_in_bytes: 185610240 Steal ticks since vm start: 0 Steal ticks percentage since vm start: 0.000 CPU:total 8 (initial active 1) (4 cores per cpu, 2 threads per core) family 6 model 94 stepping 3 microcode 0xea, cmov, cx8, fxsr, mmx, sse, sse2, sse3, ssse3, sse4.1, sse4.2, popcnt, avx, avx2, aes, clmul, erms, rtm, 3dnowpref, lzcnt, ht, tsc, tscinvbit, bmi1, bmi2, adx, fma CPU Model and flags from /proc/cpuinfo: model name : Intel(R) Xeon(R) CPU E3-1230 v5 @ 3.40GHz flags : fpu vme de pse tsc msr pae mce cx8 apic sep mtrr pge mca cmov pat pse36 clflush dts acpi mmx fxsr sse sse2 ss ht tm pbe syscall nx pdpe1gb rdtscp lm constant_tsc art arch_perfmon pebs bts rep_good nopl xtopology nonstop_tsc cpuid aperfmperf pni pclmulqdq dtes64 monitor ds_cpl vmx smx est tm2 ssse3 sdbg fma cx16 xtpr pdcm pcid sse4_1 sse4_2 x2apic movbe popcnt tsc_deadline_timer aes xsave avx f16c rdrand lahf_lm abm 3dnowprefetch cpuid_fault epb invpcid_single pti ssbd ibrs ibpb stibp tpr_shadow vnmi flexpriority ept vpid ept_ad fsgsbase tsc_adjust bmi1 hle avx2 smep bmi2 erms invpcid rtm mpx rdseed adx smap clflushopt intel_pt xsaveopt xsavec xgetbv1 xsaves dtherm ida arat pln pts hwp hwp_notify hwp_act_window hwp_epp md_clear flush_l1d Online cpus: 0-7 Offline cpus: BIOS frequency limitation: Frequency switch latency (ns): 0 Available cpu frequencies: Current governor: powersave Core performance/turbo boost: Memory: 4k page, physical 2441404k(2260128k free), swap 0k(0k free) vm_info: OpenJDK 64-Bit Server VM (11.0.13+8-Ubuntu-0ubuntu1.20.04) for linux-amd64 JRE (11.0.13+8-Ubuntu-0ubuntu1.20.04), built on Oct 29 2021 09:11:30 by "unknown" with gcc 9.3.0 END.
kfriedberger
commented
2 years ago I could not reproduce the segfault reported in the last comment. Can you tell me whether you need an updated version of JavaSMT for CPAchecker? In that case, we need to backport some bugfixes and deploy an intermediate branching version, because we can not update SMTInterpol in CPAchecker, and the newest JavaSMT would bring a new SMTInterpol.
lembergerth
commented
2 years ago I could not reproduce the segfault reported in the last comment.
Me neither. It only happened on the verifier cloud.
Can you tell me whether you need an updated version of JavaSMT for CPAchecker?
Depends on what time-frame we are talking about for a proper next version with the fix. It would be great if this could be fixed within the coming months, but it's not urgent for the foreseeable future.
Running this code in CPAchecker, which uses java-smt, crashes:
with
a2 == "|main::a@2|"and thisformula:The issue seems to be in
Dumped log: hs_err_pid28978.log
I'm not sure how to debug further. Maybe someone can give some pointers?
If you want to reproduce in CPAchecker, I've used the following command line:
and
loop-simple/nested_2.cis this program:Expand