Skip to content

Replace CVC4 by bitwuzla and CVC5 - #792

Draft
schuessf wants to merge 13 commits into
devfrom
wip/fs/bitwuzla2
Draft

Replace CVC4 by bitwuzla and CVC5#792
schuessf wants to merge 13 commits into
devfrom
wip/fs/bitwuzla2

Add cvc5 check to wrapper script again

260603f
Select commit
Loading
Failed to load commit list.
Refresh
Ultimate Jenkins CI / Tests / Build and run nightly tests failed Sep 8, 2026 in 0s

failed: 148, skipped: 133, passed: 10931

failed: 148, skipped: 133, passed: 10931

Details

de.uni_freiburg.informatik.ultimate.regressiontest.generic.ChcRegressionTestSuite.I_smtlib_horn_regression_simple_mutex_simple.smt2 S_smtlib_horn_regression_simple_ChcSolver_Golem.epf T_smtlib_horn_regression_simple_ChcSolver.xml

expected: SAT actual: CRASH   most significant results: [de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_7780330816414737079.smt2 (2621) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)]
Stack trace 
de.uni_freiburg.informatik.ultimate.test.UltimateTestFailureException: expected: SAT actual: CRASH   most significant results: [de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_7780330816414737079.smt2 (2621) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)]
Standard error 
java.lang.ClassNotFoundException: org.glassfish.jaxb.runtime.v2.JAXBContextFactory cannot be found by com.sun.xml.bind.jaxb-osgi.source_4.0.5
	at org.eclipse.osgi.internal.loader.BundleLoader.generateException(BundleLoader.java:567)
	at org.eclipse.osgi.internal.loader.BundleLoader.findClass0(BundleLoader.java:562)
	at org.eclipse.osgi.internal.loader.BundleLoader.findClass(BundleLoader.java:438)
	at org.eclipse.osgi.internal.loader.ModuleClassLoader.loadClass(ModuleClassLoader.java:195)
	at java.base/java.lang.ClassLoader.loadClass(ClassLoader.java:526)
	at org.eclipse.osgi.internal.framework.EquinoxBundle.loadClass(EquinoxBundle.java:652)
	at org.glassfish.hk2.osgiresourcelocator.ServiceLoaderImpl.loadClassSecured(ServiceLoaderImpl.java:151)
	at org.glassfish.hk2.osgiresourcelocator.ServiceLoaderImpl.lookupProviderClasses1(ServiceLoaderImpl.java:123)
	at org.glassfish.hk2.osgiresourcelocator.ServiceLoader.lookupProviderClasses(ServiceLoader.java:109)
	at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
	at java.base/java.lang.reflect.Method.invoke(Method.java:580)
	at jakarta.xml.bind.ServiceLoaderUtil.lookupsUsingOSGiServiceLoader(ServiceLoaderUtil.java:86)
	at jakarta.xml.bind.ContextFinder.find(ContextFinder.java:325)
	at jakarta.xml.bind.JAXBContext.newInstance(JAXBContext.java:392)
	at jakarta.xml.bind.JAXBContext.newInstance(JAXBContext.java:349)
	at de.uni_freiburg.informatik.ultimate.core.lib.toolchain.ToolchainFileValidator.createJAXBContext(ToolchainFileValidator.java:122)
	at de.uni_freiburg.informatik.ultimate.core.lib.toolchain.ToolchainFileValidator.loadValidatedToolchain(ToolchainFileValidator.java:82)
	at de.uni_freiburg.informatik.ultimate.core.lib.toolchain.ToolchainData.<init>(ToolchainData.java:79)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.UltimateCore.createToolchainData(UltimateCore.java:355)
	at de.uni_freiburg.informatik.ultimate.test.UltimateStarter.selectTools(UltimateStarter.java:126)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.makeToolSelection(ToolchainManager.java:199)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:133)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
Standard out 
[2026-09-08 08:02:53,912 FATAL L244          PluginFactory]: Invalid configuration. You should have at least one IController plugin, but there are none.
[2026-09-08 08:02:53,914 WARN  L309           UltimateCore]: Controller already set! Using UltimateStarter and ignoring request to set controller to NULL (this may indicate test mode!)
[2026-09-08 08:02:53,914 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2026-09-08 08:02:55,111 INFO  L114        SettingsManager]: Loading settings from /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/trunk/examples/smtlib/horn/regression/simple/ChcSolver_Golem.epf
[2026-09-08 08:02:55,112 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2026-09-08 08:02:55,112 INFO  L151        SettingsManager]: Preferences of ChcSolver differ from their defaults:
[2026-09-08 08:02:55,112 INFO  L153        SettingsManager]:  * Produce derivation if query is UNSAT=false
[2026-09-08 08:02:55,112 INFO  L153        SettingsManager]:  * CHC solver backend=GOLEM
[2026-09-08 08:02:55,112 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2026-09-08 08:02:55,112 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2026-09-08 08:02:55,112 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2026-09-08 08:02:55,169 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
Loaded toolchain from /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/trunk/examples/smtlib/horn/regression/simple/ChcSolver.xml
[2026-09-08 08:02:55,174 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2026-09-08 08:02:55,175 INFO  L270        PluginConnector]: Initializing SmtParser...
[2026-09-08 08:02:55,175 INFO  L274        PluginConnector]: SmtParser initialized
[2026-09-08 08:02:55,175 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/trunk/examples/smtlib/horn/regression/simple/mutex_simple.smt2
[2026-09-08 08:02:55,175 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2026-09-08 08:02:55,175 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time 20000 ms
unknown
de.uni_freiburg.informatik.ultimate.source.smtparser.chc.HornClauseParserScript$1@5d50c40d
[2026-09-08 08:02:55,180 INFO  L339              SmtParser]: Successfully executed SMT file /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/trunk/examples/smtlib/horn/regression/simple/mutex_simple.smt2
[2026-09-08 08:02:55,180 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2026-09-08 08:02:55,181 INFO  L133        ToolchainWalker]: Walking toolchain with 1 elements.
[2026-09-08 08:02:55,192 INFO  L112        PluginConnector]: ------------------------ChcSolver----------------------------
[2026-09-08 08:02:55,192 INFO  L270        PluginConnector]: Initializing ChcSolver...
[2026-09-08 08:02:55,192 INFO  L274        PluginConnector]: ChcSolver initialized
[2026-09-08 08:02:55,192 INFO  L184        PluginConnector]: Executing the observer ChcSolverObserver from plugin ChcSolver for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 08.09 08:02:55" (1/1) ...
[2026-09-08 08:02:55,196 INFO  L114         GolemChcScript]: Writing script to file /tmp/golem_7780330816414737079.smt2
[2026-09-08 08:02:55,205 INFO  L189       MonitoredProcess]: No working directory specified, using /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem
[2026-09-08 08:02:55,213 INFO  L229       MonitoredProcess]: Starting monitored process 2621 with /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_7780330816414737079.smt2 (exit command is null, workingDir is null)
[2026-09-08 08:02:55,215 INFO  L290       MonitoredProcess]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_7780330816414737079.smt2 (2621)] Waiting 19976 ms for monitored process
[2026-09-08 08:02:55,270 FATAL L?                        ?]: An unrecoverable error occured during an interaction with an SMT solver:
de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_7780330816414737079.smt2 (2621) without exit command) Connection to SMT solver broken
	at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)
	at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.input(Executor.java:177)
	at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.exit(Executor.java:183)
	at de.uni_freiburg.informatik.ultimate.lib.chc.GolemChcScript.solve(GolemChcScript.java:142)
	at de.uni_freiburg.informatik.ultimate.lib.chc.GolemChcScript.solve(GolemChcScript.java:105)
	at de.uni_freiburg.informatik.ultimate.plugins.chcsolver.ChcSolverObserver.process(ChcSolverObserver.java:77)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.DFSTreeWalker.runObserver(DFSTreeWalker.java:65)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.BaseWalker.runObserver(BaseWalker.java:93)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.BaseWalker.run(BaseWalker.java:86)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runObserver(PluginConnector.java:166)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runTool(PluginConnector.java:150)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.run(PluginConnector.java:127)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.executePluginConnector(ToolchainWalker.java:233)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.processPlugin(ToolchainWalker.java:227)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walkUnprotected(ToolchainWalker.java:144)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walk(ToolchainWalker.java:106)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.processToolchain(ToolchainManager.java:319)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:145)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
Caused by: java.io.IOException: Broken pipe
	at java.base/java.io.FileOutputStream.writeBytes(Native Method)
	at java.base/java.io.FileOutputStream.write(FileOutputStream.java:367)
	at java.base/java.io.BufferedOutputStream.flushBuffer(BufferedOutputStream.java:125)
	at java.base/java.io.BufferedOutputStream.implFlush(BufferedOutputStream.java:252)
	at java.base/java.io.BufferedOutputStream.flush(BufferedOutputStream.java:246)
	at java.base/sun.nio.cs.StreamEncoder.implFlush(StreamEncoder.java:412)
	at java.base/sun.nio.cs.StreamEncoder.lockedFlush(StreamEncoder.java:214)
	at java.base/sun.nio.cs.StreamEncoder.flush(StreamEncoder.java:201)
	at java.base/java.io.OutputStreamWriter.flush(OutputStreamWriter.java:262)
	at java.base/java.io.BufferedWriter.implFlush(BufferedWriter.java:372)
	at java.base/java.io.BufferedWriter.flush(BufferedWriter.java:359)
	at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.input(Executor.java:175)
	... 17 more
[2026-09-08 08:02:55,270 INFO  L158              Benchmark]: Toolchain (without parser) took 89.96ms. Allocated memory is still 601.9MB. Free memory was 134.9MB in the beginning and 121.3MB in the end (delta: 13.6MB). Peak memory consumption was 12.6MB. Max. memory is 4.3GB.
[2026-09-08 08:02:55,270 INFO  L158              Benchmark]: SmtParser took 0.01ms. Allocated memory is still 601.9MB. Free memory is still 135.8MB. There was no memory consumed. Max. memory is 4.3GB.
[2026-09-08 08:02:55,270 INFO  L158              Benchmark]: ChcSolver took 77.57ms. Allocated memory is still 601.9MB. Free memory was 127.5MB in the beginning and 121.3MB in the end (delta: 6.2MB). Peak memory consumption was 6.3MB. Max. memory is 4.3GB.
[2026-09-08 08:02:55,270 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - AssertionsEnabledResult: Assertions are enabled
    Assertions are enabled
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.01ms. Allocated memory is still 601.9MB. Free memory is still 135.8MB. There was no memory consumed. Max. memory is 4.3GB.
 * ChcSolver took 77.57ms. Allocated memory is still 601.9MB. Free memory was 127.5MB in the beginning and 121.3MB in the end (delta: 6.2MB). Peak memory consumption was 6.3MB. Max. memory is 4.3GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.chcsolver:
  - ExceptionOrErrorResult: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_7780330816414737079.smt2 (2621) without exit command) Connection to SMT solver broken
    de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_7780330816414737079.smt2 (2621) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)
[2026-09-08 08:02:55,275 INFO  L118       UltimateTestCase]: Deciding this test: ChcTestResultDecider
[2026-09-08 08:02:55,275 INFO  L431               TestUtil]: #################### TEST RESULT ####################
[2026-09-08 08:02:55,275 INFO  L431               TestUtil]: Results for Input:smtlib/horn/regression/simple/mutex_simple.smt2 Settings:smtlib/horn/regression/simple/ChcSolver_Golem.epf Toolchain:smtlib/horn/regression/simple/ChcSolver.xml
[2026-09-08 08:02:55,275 INFO  L431               TestUtil]: [0] de.uni_freiburg.informatik.ultimate.core --> [AssertionsEnabledResult] Assertions are enabled
[2026-09-08 08:02:55,275 INFO  L431               TestUtil]: [1] de.uni_freiburg.informatik.ultimate.core --> [StatisticsResult] Benchmark results are:
 * SmtParser took 0.01ms. Allocated memory is still 601.9MB. Free memory is still 135.8MB. There was no memory consumed. Max. memory is 4.3GB.
 * ChcSolver took 77.57ms. Allocated memory is still 601.9MB. Free memory was 127.5MB in the beginning and 121.3MB in the end (delta: 6.2MB). Peak memory consumption was 6.3MB. Max. memory is 4.3GB.
[2026-09-08 08:02:55,275 INFO  L431               TestUtil]: [0] de.uni_freiburg.informatik.ultimate.plugins.chcsolver --> [ExceptionOrErrorResult] de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_7780330816414737079.smt2 (2621) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)
[2026-09-08 08:02:55,275 INFO  L431               TestUtil]: Expected: Expected result: SAT
[2026-09-08 08:02:55,275 INFO  L431               TestUtil]: Actual: most significant results: [de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_7780330816414737079.smt2 (2621) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)]
[2026-09-08 08:02:55,275 INFO  L431               TestUtil]: Test result: FAIL
[2026-09-08 08:02:55,275 INFO  L431               TestUtil]: TEST FAILED
[2026-09-08 08:02:55,275 INFO  L431               TestUtil]: Statistics: heapSize=601.9MB heapFreeSize=121.1MB heapMaxSize=4.3GB
[2026-09-08 08:02:55,275 INFO  L431               TestUtil]: #################### END TEST RESULT ####################
[2026-09-08 08:02:55,275 WARN  L435       MonitoredProcess]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_7780330816414737079.smt2 (2621)] Forcibly destroying the process
[2026-09-08 08:02:55,277 INFO  L534       MonitoredProcess]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_7780330816414737079.smt2 (2621)] Forceful destruction successful, exit code 0

de.uni_freiburg.informatik.ultimate.regressiontest.generic.ChcRegressionTestSuite.I_smtlib_horn_regression_simple_dataflow-leq-unsat.smt2 S_smtlib_horn_regression_simple_ChcSolver_Golem.epf T_smtlib_horn_regression_simple_ChcSolver.xml

expected: UNSAT actual: CRASH   most significant results: [de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_8540830447201317637.smt2 (2624) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)]
Stack trace 
de.uni_freiburg.informatik.ultimate.test.UltimateTestFailureException: expected: UNSAT actual: CRASH   most significant results: [de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_8540830447201317637.smt2 (2624) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)]
Standard error 
java.lang.ClassNotFoundException: org.glassfish.jaxb.runtime.v2.JAXBContextFactory cannot be found by com.sun.xml.bind.jaxb-osgi.source_4.0.5
	at org.eclipse.osgi.internal.loader.BundleLoader.generateException(BundleLoader.java:567)
	at org.eclipse.osgi.internal.loader.BundleLoader.findClass0(BundleLoader.java:562)
	at org.eclipse.osgi.internal.loader.BundleLoader.findClass(BundleLoader.java:438)
	at org.eclipse.osgi.internal.loader.ModuleClassLoader.loadClass(ModuleClassLoader.java:195)
	at java.base/java.lang.ClassLoader.loadClass(ClassLoader.java:526)
	at org.eclipse.osgi.internal.framework.EquinoxBundle.loadClass(EquinoxBundle.java:652)
	at org.glassfish.hk2.osgiresourcelocator.ServiceLoaderImpl.loadClassSecured(ServiceLoaderImpl.java:151)
	at org.glassfish.hk2.osgiresourcelocator.ServiceLoaderImpl.lookupProviderClasses1(ServiceLoaderImpl.java:123)
	at org.glassfish.hk2.osgiresourcelocator.ServiceLoader.lookupProviderClasses(ServiceLoader.java:109)
	at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
	at java.base/java.lang.reflect.Method.invoke(Method.java:580)
	at jakarta.xml.bind.ServiceLoaderUtil.lookupsUsingOSGiServiceLoader(ServiceLoaderUtil.java:86)
	at jakarta.xml.bind.ContextFinder.find(ContextFinder.java:325)
	at jakarta.xml.bind.JAXBContext.newInstance(JAXBContext.java:392)
	at jakarta.xml.bind.JAXBContext.newInstance(JAXBContext.java:349)
	at de.uni_freiburg.informatik.ultimate.core.lib.toolchain.ToolchainFileValidator.createJAXBContext(ToolchainFileValidator.java:122)
	at de.uni_freiburg.informatik.ultimate.core.lib.toolchain.ToolchainFileValidator.loadValidatedToolchain(ToolchainFileValidator.java:82)
	at de.uni_freiburg.informatik.ultimate.core.lib.toolchain.ToolchainData.<init>(ToolchainData.java:79)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.UltimateCore.createToolchainData(UltimateCore.java:355)
	at de.uni_freiburg.informatik.ultimate.test.UltimateStarter.selectTools(UltimateStarter.java:126)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.makeToolSelection(ToolchainManager.java:199)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:133)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
Standard out 
[2026-09-08 08:02:59,676 FATAL L244          PluginFactory]: Invalid configuration. You should have at least one IController plugin, but there are none.
[2026-09-08 08:02:59,678 WARN  L309           UltimateCore]: Controller already set! Using UltimateStarter and ignoring request to set controller to NULL (this may indicate test mode!)
[2026-09-08 08:02:59,678 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2026-09-08 08:03:01,111 INFO  L114        SettingsManager]: Loading settings from /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/trunk/examples/smtlib/horn/regression/simple/ChcSolver_Golem.epf
[2026-09-08 08:03:01,112 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2026-09-08 08:03:01,112 INFO  L151        SettingsManager]: Preferences of ChcSolver differ from their defaults:
[2026-09-08 08:03:01,112 INFO  L153        SettingsManager]:  * Produce derivation if query is UNSAT=false
[2026-09-08 08:03:01,112 INFO  L153        SettingsManager]:  * CHC solver backend=GOLEM
[2026-09-08 08:03:01,112 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2026-09-08 08:03:01,112 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2026-09-08 08:03:01,112 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2026-09-08 08:03:01,183 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
Loaded toolchain from /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/trunk/examples/smtlib/horn/regression/simple/ChcSolver.xml
[2026-09-08 08:03:01,189 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2026-09-08 08:03:01,189 INFO  L270        PluginConnector]: Initializing SmtParser...
[2026-09-08 08:03:01,189 INFO  L274        PluginConnector]: SmtParser initialized
[2026-09-08 08:03:01,189 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/trunk/examples/smtlib/horn/regression/simple/dataflow-leq-unsat.smt2
[2026-09-08 08:03:01,189 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2026-09-08 08:03:01,189 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time 20000 ms
unknown
[2026-09-08 08:03:01,192 INFO  L339              SmtParser]: Successfully executed SMT file /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/trunk/examples/smtlib/horn/regression/simple/dataflow-leq-unsat.smt2
[2026-09-08 08:03:01,193 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2026-09-08 08:03:01,194 INFO  L133        ToolchainWalker]: Walking toolchain with 1 elements.
[2026-09-08 08:03:01,209 INFO  L112        PluginConnector]: ------------------------ChcSolver----------------------------
[2026-09-08 08:03:01,209 INFO  L270        PluginConnector]: Initializing ChcSolver...
[2026-09-08 08:03:01,209 INFO  L274        PluginConnector]: ChcSolver initialized
[2026-09-08 08:03:01,209 INFO  L184        PluginConnector]: Executing the observer ChcSolverObserver from plugin ChcSolver for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 08.09 08:03:01" (1/1) ...
[2026-09-08 08:03:01,209 INFO  L114         GolemChcScript]: Writing script to file /tmp/golem_8540830447201317637.smt2
[2026-09-08 08:03:01,210 INFO  L189       MonitoredProcess]: No working directory specified, using /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem
[2026-09-08 08:03:01,212 INFO  L229       MonitoredProcess]: Starting monitored process 2624 with /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_8540830447201317637.smt2 (exit command is null, workingDir is null)
[2026-09-08 08:03:01,213 INFO  L290       MonitoredProcess]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_8540830447201317637.smt2 (2624)] Waiting 19980 ms for monitored process
[2026-09-08 08:03:01,218 FATAL L?                        ?]: An unrecoverable error occured during an interaction with an SMT solver:
de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_8540830447201317637.smt2 (2624) without exit command) Connection to SMT solver broken
	at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)
	at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.input(Executor.java:177)
	at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.exit(Executor.java:183)
	at de.uni_freiburg.informatik.ultimate.lib.chc.GolemChcScript.solve(GolemChcScript.java:142)
	at de.uni_freiburg.informatik.ultimate.lib.chc.GolemChcScript.solve(GolemChcScript.java:105)
	at de.uni_freiburg.informatik.ultimate.plugins.chcsolver.ChcSolverObserver.process(ChcSolverObserver.java:77)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.DFSTreeWalker.runObserver(DFSTreeWalker.java:65)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.BaseWalker.runObserver(BaseWalker.java:93)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.BaseWalker.run(BaseWalker.java:86)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runObserver(PluginConnector.java:166)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runTool(PluginConnector.java:150)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.run(PluginConnector.java:127)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.executePluginConnector(ToolchainWalker.java:233)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.processPlugin(ToolchainWalker.java:227)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walkUnprotected(ToolchainWalker.java:144)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walk(ToolchainWalker.java:106)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.processToolchain(ToolchainManager.java:319)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:145)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
Caused by: java.io.IOException: Broken pipe
	at java.base/java.io.FileOutputStream.writeBytes(Native Method)
	at java.base/java.io.FileOutputStream.write(FileOutputStream.java:367)
	at java.base/java.io.BufferedOutputStream.flushBuffer(BufferedOutputStream.java:125)
	at java.base/java.io.BufferedOutputStream.implFlush(BufferedOutputStream.java:252)
	at java.base/java.io.BufferedOutputStream.flush(BufferedOutputStream.java:246)
	at java.base/sun.nio.cs.StreamEncoder.implFlush(StreamEncoder.java:412)
	at java.base/sun.nio.cs.StreamEncoder.lockedFlush(StreamEncoder.java:214)
	at java.base/sun.nio.cs.StreamEncoder.flush(StreamEncoder.java:201)
	at java.base/java.io.OutputStreamWriter.flush(OutputStreamWriter.java:262)
	at java.base/java.io.BufferedWriter.implFlush(BufferedWriter.java:372)
	at java.base/java.io.BufferedWriter.flush(BufferedWriter.java:359)
	at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.input(Executor.java:175)
	... 17 more
[2026-09-08 08:03:01,218 INFO  L158              Benchmark]: Toolchain (without parser) took 25.74ms. Allocated memory is still 1.8GB. Free memory was 983.2MB in the beginning and 970.9MB in the end (delta: 12.3MB). Peak memory consumption was 12.6MB. Max. memory is 4.3GB.
[2026-09-08 08:03:01,218 INFO  L158              Benchmark]: SmtParser took 0.02ms. Allocated memory is still 1.8GB. Free memory is still 983.9MB. There was no memory consumed. Max. memory is 4.3GB.
[2026-09-08 08:03:01,218 INFO  L158              Benchmark]: ChcSolver took 9.77ms. Allocated memory is still 1.8GB. Free memory was 975.5MB in the beginning and 971.6MB in the end (delta: 3.9MB). Peak memory consumption was 4.2MB. Max. memory is 4.3GB.
[2026-09-08 08:03:01,218 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - AssertionsEnabledResult: Assertions are enabled
    Assertions are enabled
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.02ms. Allocated memory is still 1.8GB. Free memory is still 983.9MB. There was no memory consumed. Max. memory is 4.3GB.
 * ChcSolver took 9.77ms. Allocated memory is still 1.8GB. Free memory was 975.5MB in the beginning and 971.6MB in the end (delta: 3.9MB). Peak memory consumption was 4.2MB. Max. memory is 4.3GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.chcsolver:
  - ExceptionOrErrorResult: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_8540830447201317637.smt2 (2624) without exit command) Connection to SMT solver broken
    de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_8540830447201317637.smt2 (2624) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)
[2026-09-08 08:03:01,219 INFO  L118       UltimateTestCase]: Deciding this test: ChcTestResultDecider
[2026-09-08 08:03:01,219 INFO  L431               TestUtil]: #################### TEST RESULT ####################
[2026-09-08 08:03:01,219 INFO  L431               TestUtil]: Results for Input:smtlib/horn/regression/simple/dataflow-leq-unsat.smt2 Settings:smtlib/horn/regression/simple/ChcSolver_Golem.epf Toolchain:smtlib/horn/regression/simple/ChcSolver.xml
[2026-09-08 08:03:01,219 INFO  L431               TestUtil]: [0] de.uni_freiburg.informatik.ultimate.core --> [AssertionsEnabledResult] Assertions are enabled
[2026-09-08 08:03:01,219 INFO  L431               TestUtil]: [1] de.uni_freiburg.informatik.ultimate.core --> [StatisticsResult] Benchmark results are:
 * SmtParser took 0.02ms. Allocated memory is still 1.8GB. Free memory is still 983.9MB. There was no memory consumed. Max. memory is 4.3GB.
 * ChcSolver took 9.77ms. Allocated memory is still 1.8GB. Free memory was 975.5MB in the beginning and 971.6MB in the end (delta: 3.9MB). Peak memory consumption was 4.2MB. Max. memory is 4.3GB.
[2026-09-08 08:03:01,219 INFO  L431               TestUtil]: [0] de.uni_freiburg.informatik.ultimate.plugins.chcsolver --> [ExceptionOrErrorResult] de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_8540830447201317637.smt2 (2624) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)
[2026-09-08 08:03:01,219 INFO  L431               TestUtil]: Expected: Expected result: UNSAT
[2026-09-08 08:03:01,219 INFO  L431               TestUtil]: Actual: most significant results: [de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_8540830447201317637.smt2 (2624) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)]
[2026-09-08 08:03:01,219 INFO  L431               TestUtil]: Test result: FAIL
[2026-09-08 08:03:01,219 INFO  L431               TestUtil]: TEST FAILED
[2026-09-08 08:03:01,219 INFO  L431               TestUtil]: Statistics: heapSize=1.8GB heapFreeSize=970.8MB heapMaxSize=4.3GB
[2026-09-08 08:03:01,219 INFO  L431               TestUtil]: #################### END TEST RESULT ####################
[2026-09-08 08:03:01,219 WARN  L435       MonitoredProcess]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_8540830447201317637.smt2 (2624)] Forcibly destroying the process
[2026-09-08 08:03:01,219 WARN  L248           UltimateCore]: Preparing to exit Ultimate with return code 4

de.uni_freiburg.informatik.ultimate.regressiontest.generic.ChcRegressionTestSuite.I_smtlib_horn_regression_simple_test-1traceOfLength4-sat.smt2 S_smtlib_horn_regression_simple_ChcSolver_Golem.epf T_smtlib_horn_regression_simple_ChcSolver.xml

expected: SAT actual: CRASH   most significant results: [de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_370981485813850052.smt2 (2622) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)]
Stack trace 
de.uni_freiburg.informatik.ultimate.test.UltimateTestFailureException: expected: SAT actual: CRASH   most significant results: [de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_370981485813850052.smt2 (2622) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)]
Standard error 
java.lang.ClassNotFoundException: org.glassfish.jaxb.runtime.v2.JAXBContextFactory cannot be found by com.sun.xml.bind.jaxb-osgi.source_4.0.5
	at org.eclipse.osgi.internal.loader.BundleLoader.generateException(BundleLoader.java:567)
	at org.eclipse.osgi.internal.loader.BundleLoader.findClass0(BundleLoader.java:562)
	at org.eclipse.osgi.internal.loader.BundleLoader.findClass(BundleLoader.java:438)
	at org.eclipse.osgi.internal.loader.ModuleClassLoader.loadClass(ModuleClassLoader.java:195)
	at java.base/java.lang.ClassLoader.loadClass(ClassLoader.java:526)
	at org.eclipse.osgi.internal.framework.EquinoxBundle.loadClass(EquinoxBundle.java:652)
	at org.glassfish.hk2.osgiresourcelocator.ServiceLoaderImpl.loadClassSecured(ServiceLoaderImpl.java:151)
	at org.glassfish.hk2.osgiresourcelocator.ServiceLoaderImpl.lookupProviderClasses1(ServiceLoaderImpl.java:123)
	at org.glassfish.hk2.osgiresourcelocator.ServiceLoader.lookupProviderClasses(ServiceLoader.java:109)
	at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
	at java.base/java.lang.reflect.Method.invoke(Method.java:580)
	at jakarta.xml.bind.ServiceLoaderUtil.lookupsUsingOSGiServiceLoader(ServiceLoaderUtil.java:86)
	at jakarta.xml.bind.ContextFinder.find(ContextFinder.java:325)
	at jakarta.xml.bind.JAXBContext.newInstance(JAXBContext.java:392)
	at jakarta.xml.bind.JAXBContext.newInstance(JAXBContext.java:349)
	at de.uni_freiburg.informatik.ultimate.core.lib.toolchain.ToolchainFileValidator.createJAXBContext(ToolchainFileValidator.java:122)
	at de.uni_freiburg.informatik.ultimate.core.lib.toolchain.ToolchainFileValidator.loadValidatedToolchain(ToolchainFileValidator.java:82)
	at de.uni_freiburg.informatik.ultimate.core.lib.toolchain.ToolchainData.<init>(ToolchainData.java:79)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.UltimateCore.createToolchainData(UltimateCore.java:355)
	at de.uni_freiburg.informatik.ultimate.test.UltimateStarter.selectTools(UltimateStarter.java:126)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.makeToolSelection(ToolchainManager.java:199)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:133)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
Standard out 
[2026-09-08 08:02:55,278 WARN  L248           UltimateCore]: Preparing to exit Ultimate with return code 4
[2026-09-08 08:02:55,983 FATAL L244          PluginFactory]: Invalid configuration. You should have at least one IController plugin, but there are none.
[2026-09-08 08:02:55,983 WARN  L309           UltimateCore]: Controller already set! Using UltimateStarter and ignoring request to set controller to NULL (this may indicate test mode!)
[2026-09-08 08:02:55,983 INFO  L188        SettingsManager]: Resetting all preferences to default values...
[2026-09-08 08:02:57,131 INFO  L114        SettingsManager]: Loading settings from /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/trunk/examples/smtlib/horn/regression/simple/ChcSolver_Golem.epf
[2026-09-08 08:02:57,132 INFO  L130        SettingsManager]: Preferences different from defaults after loading the file:
[2026-09-08 08:02:57,132 INFO  L151        SettingsManager]: Preferences of ChcSolver differ from their defaults:
[2026-09-08 08:02:57,132 INFO  L153        SettingsManager]:  * Produce derivation if query is UNSAT=false
[2026-09-08 08:02:57,132 INFO  L153        SettingsManager]:  * CHC solver backend=GOLEM
[2026-09-08 08:02:57,132 INFO  L151        SettingsManager]: Preferences of SmtParser differ from their defaults:
[2026-09-08 08:02:57,132 INFO  L153        SettingsManager]:  * SmtParser Mode=UltimateTreeAutomizer
[2026-09-08 08:02:57,133 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2026-09-08 08:02:57,188 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
Loaded toolchain from /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/trunk/examples/smtlib/horn/regression/simple/ChcSolver.xml
[2026-09-08 08:02:57,193 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2026-09-08 08:02:57,193 INFO  L270        PluginConnector]: Initializing SmtParser...
[2026-09-08 08:02:57,193 INFO  L274        PluginConnector]: SmtParser initialized
[2026-09-08 08:02:57,193 INFO  L431   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/trunk/examples/smtlib/horn/regression/simple/test-1traceOfLength4-sat.smt2
[2026-09-08 08:02:57,193 INFO  L314              SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2026-09-08 08:02:57,193 INFO  L127          SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time 20000 ms
unknown
[2026-09-08 08:02:57,196 INFO  L339              SmtParser]: Successfully executed SMT file /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/trunk/examples/smtlib/horn/regression/simple/test-1traceOfLength4-sat.smt2
[2026-09-08 08:02:57,196 INFO  L299   ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2026-09-08 08:02:57,197 INFO  L133        ToolchainWalker]: Walking toolchain with 1 elements.
[2026-09-08 08:02:57,208 INFO  L112        PluginConnector]: ------------------------ChcSolver----------------------------
[2026-09-08 08:02:57,208 INFO  L270        PluginConnector]: Initializing ChcSolver...
[2026-09-08 08:02:57,208 INFO  L274        PluginConnector]: ChcSolver initialized
[2026-09-08 08:02:57,209 INFO  L184        PluginConnector]: Executing the observer ChcSolverObserver from plugin ChcSolver for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 08.09 08:02:57" (1/1) ...
[2026-09-08 08:02:57,209 INFO  L114         GolemChcScript]: Writing script to file /tmp/golem_370981485813850052.smt2
[2026-09-08 08:02:57,210 INFO  L189       MonitoredProcess]: No working directory specified, using /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem
[2026-09-08 08:02:57,211 INFO  L229       MonitoredProcess]: Starting monitored process 2622 with /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_370981485813850052.smt2 (exit command is null, workingDir is null)
[2026-09-08 08:02:57,212 INFO  L290       MonitoredProcess]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_370981485813850052.smt2 (2622)] Waiting 19984 ms for monitored process
[2026-09-08 08:02:57,212 FATAL L?                        ?]: An unrecoverable error occured during an interaction with an SMT solver:
de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_370981485813850052.smt2 (2622) without exit command) Connection to SMT solver broken
	at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)
	at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.input(Executor.java:177)
	at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.exit(Executor.java:183)
	at de.uni_freiburg.informatik.ultimate.lib.chc.GolemChcScript.solve(GolemChcScript.java:142)
	at de.uni_freiburg.informatik.ultimate.lib.chc.GolemChcScript.solve(GolemChcScript.java:105)
	at de.uni_freiburg.informatik.ultimate.plugins.chcsolver.ChcSolverObserver.process(ChcSolverObserver.java:77)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.DFSTreeWalker.runObserver(DFSTreeWalker.java:65)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.BaseWalker.runObserver(BaseWalker.java:93)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.modelwalker.BaseWalker.run(BaseWalker.java:86)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runObserver(PluginConnector.java:166)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runTool(PluginConnector.java:150)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.run(PluginConnector.java:127)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.executePluginConnector(ToolchainWalker.java:233)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.processPlugin(ToolchainWalker.java:227)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walkUnprotected(ToolchainWalker.java:144)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walk(ToolchainWalker.java:106)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.processToolchain(ToolchainManager.java:319)
	at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:145)
	at org.eclipse.core.internal.jobs.Worker.run(Worker.java:63)
Caused by: java.io.IOException: Broken pipe
	at java.base/java.io.FileOutputStream.writeBytes(Native Method)
	at java.base/java.io.FileOutputStream.write(FileOutputStream.java:367)
	at java.base/java.io.BufferedOutputStream.flushBuffer(BufferedOutputStream.java:125)
	at java.base/java.io.BufferedOutputStream.implFlush(BufferedOutputStream.java:252)
	at java.base/java.io.BufferedOutputStream.flush(BufferedOutputStream.java:246)
	at java.base/sun.nio.cs.StreamEncoder.implFlush(StreamEncoder.java:412)
	at java.base/sun.nio.cs.StreamEncoder.lockedFlush(StreamEncoder.java:214)
	at java.base/sun.nio.cs.StreamEncoder.flush(StreamEncoder.java:201)
	at java.base/java.io.OutputStreamWriter.flush(OutputStreamWriter.java:262)
	at java.base/java.io.BufferedWriter.implFlush(BufferedWriter.java:372)
	at java.base/java.io.BufferedWriter.flush(BufferedWriter.java:359)
	at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.input(Executor.java:175)
	... 17 more
[2026-09-08 08:02:57,213 INFO  L158              Benchmark]: Toolchain (without parser) took 16.84ms. Allocated memory is still 601.9MB. Free memory was 137.8MB in the beginning and 125.2MB in the end (delta: 12.6MB). Peak memory consumption was 12.6MB. Max. memory is 4.3GB.
[2026-09-08 08:02:57,213 INFO  L158              Benchmark]: SmtParser took 0.01ms. Allocated memory is still 601.9MB. Free memory is still 137.8MB. There was no memory consumed. Max. memory is 4.3GB.
[2026-09-08 08:02:57,213 INFO  L158              Benchmark]: ChcSolver took 4.38ms. Allocated memory is still 601.9MB. Free memory was 130.4MB in the beginning and 125.2MB in the end (delta: 5.2MB). Peak memory consumption was 4.2MB. Max. memory is 4.3GB.
[2026-09-08 08:02:57,213 INFO  L338   ainManager$Toolchain]: #######################  End [Toolchain 1] #######################
 --- Results ---
 * Results from de.uni_freiburg.informatik.ultimate.core:
  - AssertionsEnabledResult: Assertions are enabled
    Assertions are enabled
  - StatisticsResult: Toolchain Benchmarks
    Benchmark results are:
 * SmtParser took 0.01ms. Allocated memory is still 601.9MB. Free memory is still 137.8MB. There was no memory consumed. Max. memory is 4.3GB.
 * ChcSolver took 4.38ms. Allocated memory is still 601.9MB. Free memory was 130.4MB in the beginning and 125.2MB in the end (delta: 5.2MB). Peak memory consumption was 4.2MB. Max. memory is 4.3GB.
 * Results from de.uni_freiburg.informatik.ultimate.plugins.chcsolver:
  - ExceptionOrErrorResult: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_370981485813850052.smt2 (2622) without exit command) Connection to SMT solver broken
    de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_370981485813850052.smt2 (2622) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)
[2026-09-08 08:02:57,213 INFO  L534       MonitoredProcess]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_370981485813850052.smt2 (2622)] Forceful destruction successful, exit code 0
[2026-09-08 08:02:57,213 INFO  L118       UltimateTestCase]: Deciding this test: ChcTestResultDecider
[2026-09-08 08:02:57,213 INFO  L431               TestUtil]: #################### TEST RESULT ####################
[2026-09-08 08:02:57,213 INFO  L431               TestUtil]: Results for Input:smtlib/horn/regression/simple/test-1traceOfLength4-sat.smt2 Settings:smtlib/horn/regression/simple/ChcSolver_Golem.epf Toolchain:smtlib/horn/regression/simple/ChcSolver.xml
[2026-09-08 08:02:57,213 INFO  L431               TestUtil]: [0] de.uni_freiburg.informatik.ultimate.core --> [AssertionsEnabledResult] Assertions are enabled
[2026-09-08 08:02:57,213 INFO  L431               TestUtil]: [1] de.uni_freiburg.informatik.ultimate.core --> [StatisticsResult] Benchmark results are:
 * SmtParser took 0.01ms. Allocated memory is still 601.9MB. Free memory is still 137.8MB. There was no memory consumed. Max. memory is 4.3GB.
 * ChcSolver took 4.38ms. Allocated memory is still 601.9MB. Free memory was 130.4MB in the beginning and 125.2MB in the end (delta: 5.2MB). Peak memory consumption was 4.2MB. Max. memory is 4.3GB.
[2026-09-08 08:02:57,214 INFO  L431               TestUtil]: [0] de.uni_freiburg.informatik.ultimate.plugins.chcsolver --> [ExceptionOrErrorResult] de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_370981485813850052.smt2 (2622) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)
[2026-09-08 08:02:57,214 INFO  L431               TestUtil]: Expected: Expected result: SAT
[2026-09-08 08:02:57,214 INFO  L431               TestUtil]: Actual: most significant results: [de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-792/releaseScripts/default/adds/golem --print-witness /tmp/golem_370981485813850052.smt2 (2622) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)]
[2026-09-08 08:02:57,214 INFO  L431               TestUtil]: Test result: FAIL
[2026-09-08 08:02:57,214 INFO  L431               TestUtil]: TEST FAILED
[2026-09-08 08:02:57,214 INFO  L431               TestUtil]: Statistics: heapSize=601.9MB heapFreeSize=125.0MB heapMaxSize=4.3GB
[2026-09-08 08:02:57,214 INFO  L431               TestUtil]: #################### END TEST RESULT ####################
[2026-09-08 08:02:57,214 WARN  L248           UltimateCore]: Preparing to exit Ultimate with return code 4

more test results are not shown here, view them on Jenkins

View more details on Ultimate Jenkins CI