Add workaround for misparsed casts #767
Draft
Ultimate Jenkins CI / Tests / Build and run nightly tests
failed
Dec 17, 2025 in 0s
failed: 80, skipped: 133, passed: 10953
failed: 80, skipped: 133, passed: 10953
Details
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: NullPointerException: Cannot invoke "java.lang.Process.getOutputStream()" because "this.mProcess" is null: de.uni_freiburg.informatik.ultimate.core.lib.util.MonitoredProcess.getOutputStream(MonitoredProcess.java:473)]
Stack trace
de.uni_freiburg.informatik.ultimate.test.UltimateTestFailureException: expected: SAT actual: CRASH most significant results: [de.uni_freiburg.informatik.ultimate.plugins.chcsolver: NullPointerException: Cannot invoke "java.lang.Process.getOutputStream()" because "this.mProcess" is null: de.uni_freiburg.informatik.ultimate.core.lib.util.MonitoredProcess.getOutputStream(MonitoredProcess.java:473)]
Standard out
[2025-12-17 03:33:13,900 FATAL L244 PluginFactory]: Invalid configuration. You should have at least one IController plugin, but there are none.
[2025-12-17 03:33:13,901 WARN L309 UltimateCore]: Controller already set! Using UltimateStarter and ignoring request to set controller to NULL (this may indicate test mode!)
[2025-12-17 03:33:13,901 INFO L188 SettingsManager]: Resetting all preferences to default values...
[2025-12-17 03:33:14,907 INFO L114 SettingsManager]: Loading settings from /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/trunk/examples/smtlib/horn/regression/simple/ChcSolver_Golem.epf
[2025-12-17 03:33:14,908 INFO L130 SettingsManager]: Preferences different from defaults after loading the file:
[2025-12-17 03:33:14,908 INFO L151 SettingsManager]: Preferences of ChcSolver differ from their defaults:
[2025-12-17 03:33:14,908 INFO L153 SettingsManager]: * Produce derivation if query is UNSAT=false
[2025-12-17 03:33:14,908 INFO L153 SettingsManager]: * CHC solver backend=GOLEM
[2025-12-17 03:33:14,908 INFO L151 SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-12-17 03:33:14,908 INFO L153 SettingsManager]: * SmtParser Mode=UltimateTreeAutomizer
[2025-12-17 03:33:14,908 INFO L75 nceAwareModelManager]: Repository-Root is: /tmp
[2025-12-17 03:33:14,955 INFO L261 ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
Loaded toolchain from /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/trunk/examples/smtlib/horn/regression/simple/ChcSolver.xml
[2025-12-17 03:33:14,959 INFO L217 ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-12-17 03:33:14,959 INFO L270 PluginConnector]: Initializing SmtParser...
[2025-12-17 03:33:14,959 INFO L274 PluginConnector]: SmtParser initialized
[2025-12-17 03:33:14,959 INFO L431 ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/trunk/examples/smtlib/horn/regression/simple/test-1traceOfLength4-sat.smt2
[2025-12-17 03:33:14,959 INFO L314 SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-12-17 03:33:14,959 INFO L127 SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time 20000 ms
unknown
[2025-12-17 03:33:14,966 INFO L339 SmtParser]: Successfully executed SMT file /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/trunk/examples/smtlib/horn/regression/simple/test-1traceOfLength4-sat.smt2
[2025-12-17 03:33:14,967 INFO L299 ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-12-17 03:33:14,968 INFO L133 ToolchainWalker]: Walking toolchain with 1 elements.
[2025-12-17 03:33:14,997 INFO L112 PluginConnector]: ------------------------ChcSolver----------------------------
[2025-12-17 03:33:14,997 INFO L270 PluginConnector]: Initializing ChcSolver...
[2025-12-17 03:33:14,997 INFO L274 PluginConnector]: ChcSolver initialized
[2025-12-17 03:33:14,997 INFO L184 PluginConnector]: Executing the observer ChcSolverObserver from plugin ChcSolver for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 17.12 03:33:14" (1/1) ...
[2025-12-17 03:33:14,997 INFO L114 GolemChcScript]: Writing script to file /tmp/golem_6503413559887172294.smt2
[2025-12-17 03:33:15,001 INFO L189 MonitoredProcess]: No working directory specified, using /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/releaseScripts/default/adds/golem
[2025-12-17 03:33:15,012 INFO L229 MonitoredProcess]: Starting monitored process 2535 with /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/releaseScripts/default/adds/golem --print-witness /tmp/golem_6503413559887172294.smt2 (exit command is null, workingDir is null)
[2025-12-17 03:33:15,013 INFO L546 MonitoredProcess]: [MP /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/releaseScripts/default/adds/golem --print-witness /tmp/golem_6503413559887172294.smt2 (2535)] Ended with exit code 0
[2025-12-17 03:33:15,015 FATAL L? ?]: The Plugin de.uni_freiburg.informatik.ultimate.plugins.chcsolver has thrown an exception:
java.lang.NullPointerException: Cannot invoke "java.lang.Process.getOutputStream()" because "this.mProcess" is null
at de.uni_freiburg.informatik.ultimate.core.lib.util.MonitoredProcess.getOutputStream(MonitoredProcess.java:473)
at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.createProcess(Executor.java:134)
at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.<init>(Executor.java:123)
at de.uni_freiburg.informatik.ultimate.lib.chc.GolemChcScript.solve(GolemChcScript.java:131)
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)
[2025-12-17 03:33:15,015 INFO L158 Benchmark]: Toolchain (without parser) took 48.39ms. Allocated memory is still 574.6MB. Free memory was 122.5MB in the beginning and 113.0MB in the end (delta: 9.4MB). Peak memory consumption was 10.5MB. Max. memory is 4.3GB.
[2025-12-17 03:33:15,015 INFO L158 Benchmark]: SmtParser took 0.01ms. Allocated memory is still 574.6MB. Free memory is still 123.5MB. There was no memory consumed. Max. memory is 4.3GB.
[2025-12-17 03:33:15,015 INFO L158 Benchmark]: ChcSolver took 18.45ms. Allocated memory is still 574.6MB. Free memory was 116.2MB in the beginning and 113.0MB in the end (delta: 3.1MB). Peak memory consumption was 4.2MB. Max. memory is 4.3GB.
[2025-12-17 03:33:15,015 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 574.6MB. Free memory is still 123.5MB. There was no memory consumed. Max. memory is 4.3GB.
* ChcSolver took 18.45ms. Allocated memory is still 574.6MB. Free memory was 116.2MB in the beginning and 113.0MB in the end (delta: 3.1MB). Peak memory consumption was 4.2MB. Max. memory is 4.3GB.
* Results from de.uni_freiburg.informatik.ultimate.plugins.chcsolver:
- ExceptionOrErrorResult: NullPointerException: Cannot invoke "java.lang.Process.getOutputStream()" because "this.mProcess" is null
de.uni_freiburg.informatik.ultimate.plugins.chcsolver: NullPointerException: Cannot invoke "java.lang.Process.getOutputStream()" because "this.mProcess" is null: de.uni_freiburg.informatik.ultimate.core.lib.util.MonitoredProcess.getOutputStream(MonitoredProcess.java:473)
[2025-12-17 03:33:15,015 INFO L118 UltimateTestCase]: Deciding this test: ChcTestResultDecider
[2025-12-17 03:33:15,016 INFO L431 TestUtil]: #################### TEST RESULT ####################
[2025-12-17 03:33:15,016 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
[2025-12-17 03:33:15,016 INFO L431 TestUtil]: [0] de.uni_freiburg.informatik.ultimate.core --> [AssertionsEnabledResult] Assertions are enabled
[2025-12-17 03:33:15,016 INFO L431 TestUtil]: [1] de.uni_freiburg.informatik.ultimate.core --> [StatisticsResult] Benchmark results are:
* SmtParser took 0.01ms. Allocated memory is still 574.6MB. Free memory is still 123.5MB. There was no memory consumed. Max. memory is 4.3GB.
* ChcSolver took 18.45ms. Allocated memory is still 574.6MB. Free memory was 116.2MB in the beginning and 113.0MB in the end (delta: 3.1MB). Peak memory consumption was 4.2MB. Max. memory is 4.3GB.
[2025-12-17 03:33:15,016 INFO L431 TestUtil]: [0] de.uni_freiburg.informatik.ultimate.plugins.chcsolver --> [ExceptionOrErrorResult] de.uni_freiburg.informatik.ultimate.plugins.chcsolver: NullPointerException: Cannot invoke "java.lang.Process.getOutputStream()" because "this.mProcess" is null: de.uni_freiburg.informatik.ultimate.core.lib.util.MonitoredProcess.getOutputStream(MonitoredProcess.java:473)
[2025-12-17 03:33:15,016 INFO L431 TestUtil]: Expected: Expected result: SAT
[2025-12-17 03:33:15,016 INFO L431 TestUtil]: Actual: most significant results: [de.uni_freiburg.informatik.ultimate.plugins.chcsolver: NullPointerException: Cannot invoke "java.lang.Process.getOutputStream()" because "this.mProcess" is null: de.uni_freiburg.informatik.ultimate.core.lib.util.MonitoredProcess.getOutputStream(MonitoredProcess.java:473)]
[2025-12-17 03:33:15,016 INFO L431 TestUtil]: Test result: FAIL
[2025-12-17 03:33:15,016 INFO L431 TestUtil]: TEST FAILED
[2025-12-17 03:33:15,016 INFO L431 TestUtil]: Statistics: heapSize=574.6MB heapFreeSize=112.9MB heapMaxSize=4.3GB
[2025-12-17 03:33:15,016 INFO L431 TestUtil]: #################### END TEST RESULT ####################
[2025-12-17 03:33:15,016 WARN L248 UltimateCore]: Preparing to exit Ultimate with return code 4
de.uni_freiburg.informatik.ultimate.regressiontest.generic.ChcRegressionTestSuite.I_smtlib_horn_regression_simple_dataflow-basic-while-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/e_Nightly_wip_fs_cast-workaround/releaseScripts/default/adds/golem --print-witness /tmp/golem_9801129577456020671.smt2 (2537) 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/e_Nightly_wip_fs_cast-workaround/releaseScripts/default/adds/golem --print-witness /tmp/golem_9801129577456020671.smt2 (2537) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)]
Standard out
[2025-12-17 03:33:17,685 FATAL L244 PluginFactory]: Invalid configuration. You should have at least one IController plugin, but there are none.
[2025-12-17 03:33:17,686 WARN L309 UltimateCore]: Controller already set! Using UltimateStarter and ignoring request to set controller to NULL (this may indicate test mode!)
[2025-12-17 03:33:17,686 INFO L188 SettingsManager]: Resetting all preferences to default values...
[2025-12-17 03:33:18,737 INFO L114 SettingsManager]: Loading settings from /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/trunk/examples/smtlib/horn/regression/simple/ChcSolver_Golem.epf
[2025-12-17 03:33:18,738 INFO L130 SettingsManager]: Preferences different from defaults after loading the file:
[2025-12-17 03:33:18,738 INFO L151 SettingsManager]: Preferences of ChcSolver differ from their defaults:
[2025-12-17 03:33:18,738 INFO L153 SettingsManager]: * Produce derivation if query is UNSAT=false
[2025-12-17 03:33:18,738 INFO L153 SettingsManager]: * CHC solver backend=GOLEM
[2025-12-17 03:33:18,738 INFO L151 SettingsManager]: Preferences of SmtParser differ from their defaults:
[2025-12-17 03:33:18,738 INFO L153 SettingsManager]: * SmtParser Mode=UltimateTreeAutomizer
[2025-12-17 03:33:18,738 INFO L75 nceAwareModelManager]: Repository-Root is: /tmp
[2025-12-17 03:33:18,786 INFO L261 ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
Loaded toolchain from /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/trunk/examples/smtlib/horn/regression/simple/ChcSolver.xml
[2025-12-17 03:33:18,789 INFO L217 ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2025-12-17 03:33:18,789 INFO L270 PluginConnector]: Initializing SmtParser...
[2025-12-17 03:33:18,790 INFO L274 PluginConnector]: SmtParser initialized
[2025-12-17 03:33:18,790 INFO L431 ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/trunk/examples/smtlib/horn/regression/simple/dataflow-basic-while-unsat.smt2
[2025-12-17 03:33:18,790 INFO L314 SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2025-12-17 03:33:18,790 INFO L127 SolverBuilder]: Constructing new instance of SMTInterpol with explicit timeout -1 ms and remaining time 19999 ms
unknown
[2025-12-17 03:33:18,794 INFO L339 SmtParser]: Successfully executed SMT file /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/trunk/examples/smtlib/horn/regression/simple/dataflow-basic-while-unsat.smt2
[2025-12-17 03:33:18,794 INFO L299 ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2025-12-17 03:33:18,796 INFO L133 ToolchainWalker]: Walking toolchain with 1 elements.
[2025-12-17 03:33:18,806 INFO L112 PluginConnector]: ------------------------ChcSolver----------------------------
[2025-12-17 03:33:18,806 INFO L270 PluginConnector]: Initializing ChcSolver...
[2025-12-17 03:33:18,806 INFO L274 PluginConnector]: ChcSolver initialized
[2025-12-17 03:33:18,806 INFO L184 PluginConnector]: Executing the observer ChcSolverObserver from plugin ChcSolver for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 17.12 03:33:18" (1/1) ...
[2025-12-17 03:33:18,806 INFO L114 GolemChcScript]: Writing script to file /tmp/golem_9801129577456020671.smt2
[2025-12-17 03:33:18,807 INFO L189 MonitoredProcess]: No working directory specified, using /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/releaseScripts/default/adds/golem
[2025-12-17 03:33:18,808 INFO L229 MonitoredProcess]: Starting monitored process 2537 with /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/releaseScripts/default/adds/golem --print-witness /tmp/golem_9801129577456020671.smt2 (exit command is null, workingDir is null)
[2025-12-17 03:33:18,811 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/e_Nightly_wip_fs_cast-workaround/releaseScripts/default/adds/golem --print-witness /tmp/golem_9801129577456020671.smt2 (2537) 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: Stream closed
at java.base/java.lang.ProcessBuilder$NullOutputStream.write(ProcessBuilder.java:447)
at java.base/java.io.OutputStream.write(OutputStream.java:167)
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
[2025-12-17 03:33:18,811 INFO L158 Benchmark]: Toolchain (without parser) took 17.16ms. Allocated memory is still 580.9MB. Free memory was 136.2MB in the beginning and 126.7MB in the end (delta: 9.4MB). Peak memory consumption was 10.5MB. Max. memory is 4.3GB.
[2025-12-17 03:33:18,811 INFO L158 Benchmark]: SmtParser took 0.01ms. Allocated memory is still 580.9MB. Free memory is still 137.2MB. There was no memory consumed. Max. memory is 4.3GB.
[2025-12-17 03:33:18,811 INFO L158 Benchmark]: ChcSolver took 5.43ms. Allocated memory is still 580.9MB. Free memory was 128.8MB in the beginning and 126.7MB in the end (delta: 2.1MB). Peak memory consumption was 4.2MB. Max. memory is 4.3GB.
[2025-12-17 03:33:18,811 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 580.9MB. Free memory is still 137.2MB. There was no memory consumed. Max. memory is 4.3GB.
* ChcSolver took 5.43ms. Allocated memory is still 580.9MB. Free memory was 128.8MB in the beginning and 126.7MB in the end (delta: 2.1MB). 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/e_Nightly_wip_fs_cast-workaround/releaseScripts/default/adds/golem --print-witness /tmp/golem_9801129577456020671.smt2 (2537) without exit command) Connection to SMT solver broken
de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/releaseScripts/default/adds/golem --print-witness /tmp/golem_9801129577456020671.smt2 (2537) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)
[2025-12-17 03:33:18,811 INFO L290 MonitoredProcess]: [MP /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/releaseScripts/default/adds/golem --print-witness /tmp/golem_9801129577456020671.smt2 (2537)] Waiting 19982 ms for monitored process
[2025-12-17 03:33:18,812 INFO L534 MonitoredProcess]: [MP /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/releaseScripts/default/adds/golem --print-witness /tmp/golem_9801129577456020671.smt2 (2537)] Forceful destruction successful, exit code 0
[2025-12-17 03:33:18,814 INFO L118 UltimateTestCase]: Deciding this test: ChcTestResultDecider
[2025-12-17 03:33:18,814 INFO L431 TestUtil]: #################### TEST RESULT ####################
[2025-12-17 03:33:18,814 INFO L431 TestUtil]: Results for Input:smtlib/horn/regression/simple/dataflow-basic-while-unsat.smt2 Settings:smtlib/horn/regression/simple/ChcSolver_Golem.epf Toolchain:smtlib/horn/regression/simple/ChcSolver.xml
[2025-12-17 03:33:18,814 INFO L431 TestUtil]: [0] de.uni_freiburg.informatik.ultimate.core --> [AssertionsEnabledResult] Assertions are enabled
[2025-12-17 03:33:18,814 INFO L431 TestUtil]: [1] de.uni_freiburg.informatik.ultimate.core --> [StatisticsResult] Benchmark results are:
* SmtParser took 0.01ms. Allocated memory is still 580.9MB. Free memory is still 137.2MB. There was no memory consumed. Max. memory is 4.3GB.
* ChcSolver took 5.43ms. Allocated memory is still 580.9MB. Free memory was 128.8MB in the beginning and 126.7MB in the end (delta: 2.1MB). Peak memory consumption was 4.2MB. Max. memory is 4.3GB.
[2025-12-17 03:33:18,814 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/e_Nightly_wip_fs_cast-workaround/releaseScripts/default/adds/golem --print-witness /tmp/golem_9801129577456020671.smt2 (2537) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)
[2025-12-17 03:33:18,814 INFO L431 TestUtil]: Expected: Expected result: UNSAT
[2025-12-17 03:33:18,814 INFO L431 TestUtil]: Actual: most significant results: [de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/e_Nightly_wip_fs_cast-workaround/releaseScripts/default/adds/golem --print-witness /tmp/golem_9801129577456020671.smt2 (2537) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)]
[2025-12-17 03:33:18,814 INFO L431 TestUtil]: Test result: FAIL
[2025-12-17 03:33:18,814 INFO L431 TestUtil]: TEST FAILED
[2025-12-17 03:33:18,814 INFO L431 TestUtil]: Statistics: heapSize=580.9MB heapFreeSize=125.5MB heapMaxSize=4.3GB
[2025-12-17 03:33:18,814 INFO L431 TestUtil]: #################### END TEST RESULT ####################
more test results are not shown here, view them on Jenkins
Loading