[CVC5 on Windows] SegFault when creating multiple CVC5 instances

[kfriedberger]

CVC5 on Windows crashes in special cases, mostly related to creating several instances within a short timeframe.
There are several examples in current Appveyor builds, mostly related to TimeoutTest or SolverConcurrencyTest.

Example:

testCVC5WithValidOptionsTimeLimit in SolverContextTest

Version:

• JavaSMT from f929bdc (before change f071868).
• CVC5 from Ivy, 1.2.1-g8594a8e4dc, cross-compiled on Linux with our current Ant build scripts.

The quick fix (not a real fix!) was to disable the test on Windows: f071868

Log for the SegFault (JavaVM/JUnit hangs forever after the SegFault):

# A fatal error has been detected by the Java Runtime Environment:
#
#  EXCEPTION_ACCESS_VIOLATION (0xc0000005) at pc=0x00007ffa7c20f4e1, pid=11460, tid=7812
#
# JRE version: OpenJDK Runtime Environment Corretto-22.0.2.9.1 (22.0.2+9) (build 22.0.2+9-FR)
# Java VM: OpenJDK 64-Bit Server VM Corretto-22.0.2.9.1 (22.0.2+9-FR, mixed mode, sharing, tiered, compressed oops, compressed class ptrs, g1 gc, windows-amd64)
# Problematic frame:
# C  [ntdll.dll+0x3f4e1]
#
# No core dump will be written. Minidumps are not enabled by default on client versions of Windows
#
# If you would like to submit a bug report, please visit:
#   https://github.com/corretto/corretto-22/issues/
# 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: -ea -Didea.test.cyclic.buffer.size=1048576 -javaagent:C:\Users\friedk\AppData\Local\JetBrains\IntelliJ IDEA Community Edition 2024.1.4\lib\idea_rt.jar=52144:C:\Users\friedk\AppData\Local\JetBrains\IntelliJ IDEA Community Edition 2024.1.4\bin -javaagent:C:\Users\friedk\AppData\Local\JetBrains\IdeaIC2024.3\captureAgent\debugger-agent.jar -Dkotlinx.coroutines.debug.enable.creation.stack.trace=false -Ddebugger.agent.enable.coroutines=true -Dkotlinx.coroutines.debug.enable.flows.stack.trace=true -Dkotlinx.coroutines.debug.enable.mutable.state.flows.stack.trace=true -Dfile.encoding=UTF-8 -Dsun.stdout.encoding=UTF-8 -Dsun.stderr.encoding=UTF-8 com.intellij.rt.junit.JUnitStarter -ideVersion5 -junit4 org.sosy_lab.java_smt.test.SolverContextTest

Host: 11th Gen Intel(R) Core(TM) i7-11850H @ 2.50GHz, 16 cores, 63G,  Windows 11 , 64 bit Build 22621 (10.0.22621.4974)
Time: Sat Mar 29 09:24:53 2025 Mitteleuropäische Zeit elapsed time: 3.159949 seconds (0d 0h 0m 3s)

---------------  T H R E A D  ---------------

Current thread (0x0000023ce4e4f5f0):  JavaThread "main"             [_thread_in_native, id=7812, stack(0x000000c840500000,0x000000c840600000) (1024K)]

Stack: [0x000000c840500000,0x000000c840600000],  sp=0x000000c8405fdc00,  free space=1015k
Native frames: (J=compiled Java code, j=interpreted, Vv=VM code, C=native code)
C  [ntdll.dll+0x3f4e1]  (no source info available)
C  [ntdll.dll+0x3d249]  (no source info available)
C  [msvcrt.dll+0x1cb80]  (no source info available)
C  [libcvc5jni.dll+0x15cd489]  (no source info available)
C  [libcvc5jni.dll+0x12d7a6]  (no source info available)
C  [libcvc5jni.dll+0x163060]  (no source info available)
C  [libcvc5jni.dll+0xa63fd]  (no source info available)
C  [libcvc5jni.dll+0xa653d]  (no source info available)
C  [libcvc5jni.dll+0x10f89]  (no source info available)
C  0x0000023cf6b4d0c7  (no source info available)

The last pc belongs to native method entry point (kind = native) (printed below).
Java frames: (J=compiled Java code, j=interpreted, Vv=VM code)
j  io.github.cvc5.Solver.newSolver(J)J+0
j  io.github.cvc5.Solver.<init>(Lio/github/cvc5/TermManager;)V+5
j  org.sosy_lab.java_smt.solvers.cvc5.CVC5SolverContext.create(Lorg/sosy_lab/common/log/LogManager;Lorg/sosy_lab/common/configuration/Configuration;Lorg/sosy_lab/common/ShutdownNotifier;ILorg/sosy_lab/java_smt/basicimpl/AbstractNumeralFormulaManager$NonLinearArithmetic;Lorg/sosy_lab/java_smt/api/FloatingPointRoundingMode;Ljava/util/function/Consumer;)Lorg/sosy_lab/java_smt/api/SolverContext;+30
j  org.sosy_lab.java_smt.SolverContextFactory.generateContext0(Lorg/sosy_lab/java_smt/SolverContextFactory$Solvers;)Lorg/sosy_lab/java_smt/api/SolverContext;+146
j  org.sosy_lab.java_smt.SolverContextFactory.generateContext(Lorg/sosy_lab/java_smt/SolverContextFactory$Solvers;)Lorg/sosy_lab/java_smt/api/SolverContext;+2
j  org.sosy_lab.java_smt.SolverContextFactory.generateContext()Lorg/sosy_lab/java_smt/api/SolverContext;+5
j  org.sosy_lab.java_smt.test.SolverBasedTest0.initSolver()V+39
j  java.lang.invoke.DirectMethodHandle$Holder.invokeSpecial(Ljava/lang/Object;Ljava/lang/Object;)V+10 java.base@22.0.2
j  java.lang.invoke.LambdaForm$MH+0x0000023c9702c800.invoke(Ljava/lang/Object;Ljava/lang/Object;)Ljava/lang/Object;+31 java.base@22.0.2
J 1453 c1 java.lang.invoke.Invokers$Holder.invokeExact_MT(Ljava/lang/Object;Ljava/lang/Object;Ljava/lang/Object;)Ljava/lang/Object; java.base@22.0.2 (23 bytes) @ 0x0000023cef95e52c [0x0000023cef95df20+0x000000000000060c]
j  jdk.internal.reflect.DirectMethodHandleAccessor.invokeImpl(Ljava/lang/Object;[Ljava/lang/Object;)Ljava/lang/Object;+41 java.base@22.0.2
j  jdk.internal.reflect.DirectMethodHandleAccessor.invoke(Ljava/lang/Object;[Ljava/lang/Object;)Ljava/lang/Object;+23 java.base@22.0.2
j  java.lang.reflect.Method.invoke(Ljava/lang/Object;[Ljava/lang/Object;)Ljava/lang/Object;+102 java.base@22.0.2
j  org.junit.runners.model.FrameworkMethod$1.runReflectiveCall()Ljava/lang/Object;+15
j  org.junit.internal.runners.model.ReflectiveCallable.run()Ljava/lang/Object;+1
j  org.junit.runners.model.FrameworkMethod.invokeExplosively(Ljava/lang/Object;[Ljava/lang/Object;)Ljava/lang/Object;+10
j  org.junit.internal.runners.statements.RunBefores.invokeMethod(Lorg/junit/runners/model/FrameworkMethod;)V+9
j  org.junit.internal.runners.statements.RunBefores.evaluate()V+31
j  org.junit.internal.runners.statements.RunAfters.evaluate()V+12
j  org.junit.runners.ParentRunner$3.evaluate()V+4
j  org.junit.runners.BlockJUnit4ClassRunner$1.evaluate()V+11
j  org.junit.runners.ParentRunner.runLeaf(Lorg/junit/runners/model/Statement;Lorg/junit/runner/Description;Lorg/junit/runner/notification/RunNotifier;)V+17
j  org.junit.runners.BlockJUnit4ClassRunner.runChild(Lorg/junit/runners/model/FrameworkMethod;Lorg/junit/runner/notification/RunNotifier;)V+38
j  org.junit.runners.BlockJUnit4ClassRunner.runChild(Ljava/lang/Object;Lorg/junit/runner/notification/RunNotifier;)V+6
j  org.junit.runners.ParentRunner$4.run()V+12
j  org.junit.runners.ParentRunner$1.schedule(Ljava/lang/Runnable;)V+1
j  org.junit.runners.ParentRunner.runChildren(Lorg/junit/runner/notification/RunNotifier;)V+44
j  org.junit.runners.ParentRunner.access$100(Lorg/junit/runners/ParentRunner;Lorg/junit/runner/notification/RunNotifier;)V+2
j  org.junit.runners.ParentRunner$2.evaluate()V+8
j  org.junit.runners.ParentRunner.run(Lorg/junit/runner/notification/RunNotifier;)V+24
j  org.junit.runners.Suite.runChild(Lorg/junit/runner/Runner;Lorg/junit/runner/notification/RunNotifier;)V+2
j  org.junit.runners.Suite.runChild(Ljava/lang/Object;Lorg/junit/runner/notification/RunNotifier;)V+6
j  org.junit.runners.ParentRunner$4.run()V+12
j  org.junit.runners.ParentRunner$1.schedule(Ljava/lang/Runnable;)V+1
j  org.junit.runners.ParentRunner.runChildren(Lorg/junit/runner/notification/RunNotifier;)V+44
j  org.junit.runners.ParentRunner.access$100(Lorg/junit/runners/ParentRunner;Lorg/junit/runner/notification/RunNotifier;)V+2
j  org.junit.runners.ParentRunner$2.evaluate()V+8
j  org.junit.runners.ParentRunner$3.evaluate()V+4
j  org.junit.runners.ParentRunner.run(Lorg/junit/runner/notification/RunNotifier;)V+24
j  org.junit.runner.JUnitCore.run(Lorg/junit/runner/Runner;)Lorg/junit/runner/Result;+37
j  com.intellij.junit4.JUnit4IdeaTestRunner.startRunnerWithArgs([Ljava/lang/String;Ljava/lang/String;IZ)I+166
j  com.intellij.rt.junit.IdeaTestRunner$Repeater$1.execute(Z)I+17
j  com.intellij.rt.execution.junit.TestsRepeater.repeat(IZLcom/intellij/rt/execution/junit/TestsRepeater$TestRun;)I+7
j  com.intellij.rt.junit.IdeaTestRunner$Repeater.startRunnerWithArgs(Lcom/intellij/rt/junit/IdeaTestRunner;[Ljava/lang/String;Ljava/util/ArrayList;Ljava/lang/String;IZ)I+25
j  com.intellij.rt.junit.JUnitStarter.prepareStreamsAndStart([Ljava/lang/String;Ljava/lang/String;Ljava/util/ArrayList;Ljava/lang/String;)I+117
j  com.intellij.rt.junit.JUnitStarter.main([Ljava/lang/String;)V+97
v  ~StubRoutines::call_stub 0x0000023cf6b4100d
[...]

[shivammm21]

/assign @shivammm21

Hi, I’m looking into the issue with CVC5 on Windows where it crashes when creating multiple instances. I'll try increasing the timeout, checking memory usage, and debugging the native code. I’ll also ensure all dependencies are up to date and rebuild CVC5 with debug symbols. I’ll update here with my progress.

[daniel-raffler]

/assign @shivammm21

Hi, I’m looking into the issue with CVC5 on Windows where it crashes when creating multiple instances. I'll try increasing the timeout, checking memory usage, and debugging the native code. I’ll also ensure all dependencies are up to date and rebuild CVC5 with debug symbols. I’ll update here with my progress.

Hello Shivam,
thanks for offering your help! I think this issue might be linked to a bug I reported here some time ago. Maybe you could start by checking if the patch fixes it? CVC5 has problems with concurrency in general (see here) and this often makes these problems hard to debug. They are working on a solution, but it will likely still take some time.

[kfriedberger]

This issue is fixed with the update of CVC5 in #480. The tests are re-enabled in #484.