Always use IcfgBuilder and remove RCFGBuilder
#770
Ultimate Jenkins CI / Tests / Build and run nightly tests
failed
May 22, 2026 in 0s
failed: 74, skipped: 133, passed: 10959
failed: 74, skipped: 133, passed: 10959
Details
de.uni_freiburg.informatik.ultimate.regressiontest.generic.ChcRegressionTestSuite.I_smtlib_horn_regression_simple_mutex_with_counter.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-770/releaseScripts/default/adds/golem --print-witness /tmp/golem_5353984439053716430.smt2 (2538) 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-770/releaseScripts/default/adds/golem --print-witness /tmp/golem_5353984439053716430.smt2 (2538) 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-05-22 01:41:10,550 FATAL L244 PluginFactory]: Invalid configuration. You should have at least one IController plugin, but there are none.
[2026-05-22 01:41:10,551 WARN L309 UltimateCore]: Controller already set! Using UltimateStarter and ignoring request to set controller to NULL (this may indicate test mode!)
[2026-05-22 01:41:10,551 INFO L188 SettingsManager]: Resetting all preferences to default values...
[2026-05-22 01:41:11,245 INFO L114 SettingsManager]: Loading settings from /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/trunk/examples/smtlib/horn/regression/simple/ChcSolver_Golem.epf
[2026-05-22 01:41:11,246 INFO L130 SettingsManager]: Preferences different from defaults after loading the file:
[2026-05-22 01:41:11,246 INFO L151 SettingsManager]: Preferences of ChcSolver differ from their defaults:
[2026-05-22 01:41:11,246 INFO L153 SettingsManager]: * Produce derivation if query is UNSAT=false
[2026-05-22 01:41:11,246 INFO L153 SettingsManager]: * CHC solver backend=GOLEM
[2026-05-22 01:41:11,246 INFO L151 SettingsManager]: Preferences of SmtParser differ from their defaults:
[2026-05-22 01:41:11,246 INFO L153 SettingsManager]: * SmtParser Mode=UltimateTreeAutomizer
[2026-05-22 01:41:11,246 INFO L75 nceAwareModelManager]: Repository-Root is: /tmp
[2026-05-22 01:41:11,279 INFO L261 ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
Loaded toolchain from /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/trunk/examples/smtlib/horn/regression/simple/ChcSolver.xml
[2026-05-22 01:41:11,284 INFO L217 ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2026-05-22 01:41:11,284 INFO L270 PluginConnector]: Initializing SmtParser...
[2026-05-22 01:41:11,284 INFO L274 PluginConnector]: SmtParser initialized
[2026-05-22 01:41:11,284 INFO L431 ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/trunk/examples/smtlib/horn/regression/simple/mutex_with_counter.smt2
[2026-05-22 01:41:11,284 INFO L314 SmtParser]: Parsing .smt2 file as a set of Horn Clauses
[2026-05-22 01:41:11,284 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@78f5d3a
[2026-05-22 01:41:11,289 INFO L339 SmtParser]: Successfully executed SMT file /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/trunk/examples/smtlib/horn/regression/simple/mutex_with_counter.smt2
[2026-05-22 01:41:11,289 INFO L299 ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2026-05-22 01:41:11,289 INFO L133 ToolchainWalker]: Walking toolchain with 1 elements.
[2026-05-22 01:41:11,296 INFO L112 PluginConnector]: ------------------------ChcSolver----------------------------
[2026-05-22 01:41:11,296 INFO L270 PluginConnector]: Initializing ChcSolver...
[2026-05-22 01:41:11,296 INFO L274 PluginConnector]: ChcSolver initialized
[2026-05-22 01:41:11,296 INFO L184 PluginConnector]: Executing the observer ChcSolverObserver from plugin ChcSolver for "de.uni_freiburg.informatik.ultimate.source.smtparser OTHER 22.05 01:41:11" (1/1) ...
[2026-05-22 01:41:11,296 INFO L114 GolemChcScript]: Writing script to file /tmp/golem_5353984439053716430.smt2
[2026-05-22 01:41:11,297 INFO L189 MonitoredProcess]: No working directory specified, using /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/golem
[2026-05-22 01:41:11,298 INFO L229 MonitoredProcess]: Starting monitored process 2538 with /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/golem --print-witness /tmp/golem_5353984439053716430.smt2 (exit command is null, workingDir is null)
[2026-05-22 01:41:11,299 INFO L290 MonitoredProcess]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/golem --print-witness /tmp/golem_5353984439053716430.smt2 (2538)] Waiting 19987 ms for monitored process
[2026-05-22 01:41:11,309 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-770/releaseScripts/default/adds/golem --print-witness /tmp/golem_5353984439053716430.smt2 (2538) 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-05-22 01:41:11,310 INFO L158 Benchmark]: Toolchain (without parser) took 20.59ms. Allocated memory is still 1.3GB. Free memory was 861.1MB in the beginning and 853.8MB in the end (delta: 7.3MB). Peak memory consumption was 6.3MB. Max. memory is 4.3GB.
[2026-05-22 01:41:11,310 INFO L158 Benchmark]: SmtParser took 0.02ms. Allocated memory is still 1.3GB. Free memory is still 862.2MB. There was no memory consumed. Max. memory is 4.3GB.
[2026-05-22 01:41:11,310 INFO L158 Benchmark]: ChcSolver took 13.83ms. Allocated memory is still 1.3GB. Free memory was 858.0MB in the beginning and 853.8MB in the end (delta: 4.2MB). Peak memory consumption was 4.2MB. Max. memory is 4.3GB.
[2026-05-22 01:41:11,310 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.3GB. Free memory is still 862.2MB. There was no memory consumed. Max. memory is 4.3GB.
* ChcSolver took 13.83ms. Allocated memory is still 1.3GB. Free memory was 858.0MB in the beginning and 853.8MB in the end (delta: 4.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-770/releaseScripts/default/adds/golem --print-witness /tmp/golem_5353984439053716430.smt2 (2538) 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-770/releaseScripts/default/adds/golem --print-witness /tmp/golem_5353984439053716430.smt2 (2538) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)
[2026-05-22 01:41:11,310 INFO L546 MonitoredProcess]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/golem --print-witness /tmp/golem_5353984439053716430.smt2 (2538)] Ended with exit code 0
[2026-05-22 01:41:11,311 INFO L118 UltimateTestCase]: Deciding this test: ChcTestResultDecider
[2026-05-22 01:41:11,311 INFO L431 TestUtil]: #################### TEST RESULT ####################
[2026-05-22 01:41:11,311 INFO L431 TestUtil]: Results for Input:smtlib/horn/regression/simple/mutex_with_counter.smt2 Settings:smtlib/horn/regression/simple/ChcSolver_Golem.epf Toolchain:smtlib/horn/regression/simple/ChcSolver.xml
[2026-05-22 01:41:11,311 INFO L431 TestUtil]: [0] de.uni_freiburg.informatik.ultimate.core --> [AssertionsEnabledResult] Assertions are enabled
[2026-05-22 01:41:11,311 INFO L431 TestUtil]: [1] de.uni_freiburg.informatik.ultimate.core --> [StatisticsResult] Benchmark results are:
* SmtParser took 0.02ms. Allocated memory is still 1.3GB. Free memory is still 862.2MB. There was no memory consumed. Max. memory is 4.3GB.
* ChcSolver took 13.83ms. Allocated memory is still 1.3GB. Free memory was 858.0MB in the beginning and 853.8MB in the end (delta: 4.2MB). Peak memory consumption was 4.2MB. Max. memory is 4.3GB.
[2026-05-22 01:41:11,311 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-770/releaseScripts/default/adds/golem --print-witness /tmp/golem_5353984439053716430.smt2 (2538) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)
[2026-05-22 01:41:11,311 INFO L431 TestUtil]: Expected: Expected result: SAT
[2026-05-22 01:41:11,311 INFO L431 TestUtil]: Actual: most significant results: [de.uni_freiburg.informatik.ultimate.plugins.chcsolver: SMTLIBException: golem (MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/golem --print-witness /tmp/golem_5353984439053716430.smt2 (2538) without exit command) Connection to SMT solver broken: de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.convertIOException(Executor.java:337)]
[2026-05-22 01:41:11,311 INFO L431 TestUtil]: Test result: FAIL
[2026-05-22 01:41:11,311 INFO L431 TestUtil]: TEST FAILED
[2026-05-22 01:41:11,311 INFO L431 TestUtil]: Statistics: heapSize=1.3GB heapFreeSize=853.6MB heapMaxSize=4.3GB
[2026-05-22 01:41:11,311 INFO L431 TestUtil]: #################### END TEST RESULT ####################
[2026-05-22 01:41:11,311 WARN L248 UltimateCore]: Preparing to exit Ultimate with return code 4
de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.PolynomialRelationTest.relationIntRecDivModEq
Insufficient resources to check soundness
Stack trace
java.lang.AssertionError: Insufficient resources to check soundness
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.PolynomialRelationTest.testMultiCaseSolveForSubject(PolynomialRelationTest.java:682)
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.PolynomialRelationTest.testSolveForXMultiCaseOnly(PolynomialRelationTest.java:651)
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.PolynomialRelationTest.relationIntRecDivModEq(PolynomialRelationTest.java:904)
Standard out
[INFO]: No working directory specified, using /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3
[INFO]: Starting monitored process 237 with /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:6000 -memory:2024 -smt2 -in smt.arith.solver=2 (exit command is (exit), workingDir is null)
[INFO]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:6000 -memory:2024 -smt2 -in smt.arith.solver=2 (237)] Waiting until timeout for monitored process
[WARN]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:6000 -memory:2024 -smt2 -in smt.arith.solver=2 (237)] Forcibly destroying the process
[INFO]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:6000 -memory:2024 -smt2 -in smt.arith.solver=2 (237)] Forceful destruction successful, exit code 0
de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.QuantifierEliminationDivMod.qeMod34DEADF0
Insufficient ressources for checking equivalence to expected result: (let ((.cse4 (mod |ULTIMATE.start_Id_MCDC_99_~Id_MCDC_140~0#1| 4294967296)) (.cse1 (+ 2 |ULTIMATE.start_Id_MCDC_99_~#Id_MCDC_139~0#1.offset|)) (.cse3 (select |#memory_int| |ULTIMATE.start_Id_MCDC_99_~#Id_MCDC_139~0#1.base|)) (.cse2 (+ 3 |ULTIMATE.start_Id_MCDC_99_~#Id_MCDC_139~0#1.offset|))) (and (let ((.cse0 (store .cse3 (+ |ULTIMATE.start_Id_MCDC_99_~#Id_MCDC_139~0#1.offset| .cse4) 1))) (<= (mod (select .cse0 .cse1) 4294967296) (mod (select .cse0 .cse2) 4294967296))) (or (< .cse4 2147483648) (< (mod (select .cse3 .cse1) 4294967296) (+ (mod (select .cse3 .cse2) 4294967296) 1)))))
Stack trace
java.lang.AssertionError: Insufficient ressources for checking equivalence to expected result: (let ((.cse4 (mod |ULTIMATE.start_Id_MCDC_99_~Id_MCDC_140~0#1| 4294967296)) (.cse1 (+ 2 |ULTIMATE.start_Id_MCDC_99_~#Id_MCDC_139~0#1.offset|)) (.cse3 (select |#memory_int| |ULTIMATE.start_Id_MCDC_99_~#Id_MCDC_139~0#1.base|)) (.cse2 (+ 3 |ULTIMATE.start_Id_MCDC_99_~#Id_MCDC_139~0#1.offset|))) (and (let ((.cse0 (store .cse3 (+ |ULTIMATE.start_Id_MCDC_99_~#Id_MCDC_139~0#1.offset| .cse4) 1))) (<= (mod (select .cse0 .cse1) 4294967296) (mod (select .cse0 .cse2) 4294967296))) (or (< .cse4 2147483648) (< (mod (select .cse3 .cse1) 4294967296) (+ (mod (select .cse3 .cse2) 4294967296) 1)))))
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.QuantifierEliminationDivMod.qeMod34DEADF0(QuantifierEliminationDivMod.java:453)
Standard out
[INFO]: No working directory specified, using /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3
[INFO]: Starting monitored process 54 with /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:1000 -memory:2024 -smt2 -in (exit command is (exit), workingDir is null)
[INFO]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:1000 -memory:2024 -smt2 -in (54)] Waiting until timeout for monitored process
[INFO]: Elimination output: (let ((.cse4 (mod |ULTIMATE.start_Id_MCDC_99_~Id_MCDC_140~0#1| 4294967296)) (.cse1 (+ 2 |ULTIMATE.start_Id_MCDC_99_~#Id_MCDC_139~0#1.offset|)) (.cse3 (select |#memory_int| |ULTIMATE.start_Id_MCDC_99_~#Id_MCDC_139~0#1.base|)) (.cse2 (+ 3 |ULTIMATE.start_Id_MCDC_99_~#Id_MCDC_139~0#1.offset|))) (and (let ((.cse0 (store .cse3 (+ |ULTIMATE.start_Id_MCDC_99_~#Id_MCDC_139~0#1.offset| .cse4) 1))) (<= (mod (select .cse0 .cse1) 4294967296) (mod (select .cse0 .cse2) 4294967296))) (or (< .cse4 2147483648) (< (mod (select .cse3 .cse1) 4294967296) (+ (mod (select .cse3 .cse2) 4294967296) 1)))))
[INFO]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:1000 -memory:2024 -smt2 -in (54)] Ended with exit code 0
de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.QuantifierEliminationRegressionTest.mod02Uneliminatable
Insufficient ressources for checking equivalence to expected result: (or (exists ((v_z_1 Int)) (and (<= v_z_1 6) (<= 0 v_z_1) (exists ((v_z_3 Int)) (and (<= v_z_3 3) (<= 0 v_z_3) (exists ((v_y_3 Int)) (and (p (+ (* 7 v_y_3) v_z_1)) (p (+ (* 5 v_y_3) (* v_z_3 1))))))))) (exists ((v_z_1 Int)) (and (<= v_z_1 6) (<= 0 v_z_1) (exists ((v_y_3 Int)) (and (p (+ 7 (* 7 v_y_3) v_z_1)) (p (+ (* 5 v_y_3) 4)))))))
Stack trace
java.lang.AssertionError: Insufficient ressources for checking equivalence to expected result: (or (exists ((v_z_1 Int)) (and (<= v_z_1 6) (<= 0 v_z_1) (exists ((v_z_3 Int)) (and (<= v_z_3 3) (<= 0 v_z_3) (exists ((v_y_3 Int)) (and (p (+ (* 7 v_y_3) v_z_1)) (p (+ (* 5 v_y_3) (* v_z_3 1))))))))) (exists ((v_z_1 Int)) (and (<= v_z_1 6) (<= 0 v_z_1) (exists ((v_y_3 Int)) (and (p (+ 7 (* 7 v_y_3) v_z_1)) (p (+ (* 5 v_y_3) 4)))))))
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.QuantifierEliminationRegressionTest.mod02Uneliminatable(QuantifierEliminationRegressionTest.java:1570)
Standard out
[INFO]: No working directory specified, using /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3
[INFO]: Starting monitored process 423 with /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:1000 -memory:2024 -smt2 -in (exit command is (exit), workingDir is null)
[INFO]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:1000 -memory:2024 -smt2 -in (423)] Waiting until timeout for monitored process
[INFO]: Elimination output: (or (exists ((v_z_1 Int)) (and (<= v_z_1 6) (<= 0 v_z_1) (exists ((v_z_3 Int)) (and (<= v_z_3 3) (<= 0 v_z_3) (exists ((v_y_3 Int)) (and (p (+ (* 7 v_y_3) v_z_1)) (p (+ (* 5 v_y_3) (* v_z_3 1))))))))) (exists ((v_z_1 Int)) (and (<= v_z_1 6) (<= 0 v_z_1) (exists ((v_y_3 Int)) (and (p (+ 7 (* 7 v_y_3) v_z_1)) (p (+ (* 5 v_y_3) 4)))))))
[INFO]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:1000 -memory:2024 -smt2 -in (423)] Ended with exit code 0
de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.QuantifierEliminationRegressionTest.hiddenWeakArrayEquality08SomeBug
Elimination output is quantifier-free
Stack trace
java.lang.AssertionError: Elimination output is quantifier-free
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.QuantifierEliminationRegressionTest.hiddenWeakArrayEquality08SomeBug(QuantifierEliminationRegressionTest.java:566)
Standard out
[INFO]: No working directory specified, using /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3
[INFO]: Starting monitored process 485 with /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:1000 -memory:2024 -smt2 -in (exit command is (exit), workingDir is null)
[INFO]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:1000 -memory:2024 -smt2 -in (485)] Waiting until timeout for monitored process
[INFO]: treesize reduction 26, result has 3.7 percent of original size
[INFO]: Elim1 eliminated variable of array dimension 2, 1 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 2 new quantified variables, introduced 1 case distinctions, treesize of input 33 treesize of output 20
[INFO]: Elim1 eliminated variable of array dimension 1, 1 stores, 1 select indices, 1 select index equivalence classes, 1 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 19 treesize of output 12
[INFO]: Elimination output: (not (= k (select (select mem k) 0)))
[INFO]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:1000 -memory:2024 -smt2 -in (485)] Ended with exit code 0
de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.QuantifierEliminationTest.avdiivkaSimplified
Insufficient ressources for checking equivalence to expected result: (and (= i 1048) (exists ((i Int)) (and (forall ((k Int)) (or (= 42 (select a k)) (< i (+ k 1)))) (<= i 2023))))
Stack trace
java.lang.AssertionError: Insufficient ressources for checking equivalence to expected result: (and (= i 1048) (exists ((i Int)) (and (forall ((k Int)) (or (= 42 (select a k)) (< i (+ k 1)))) (<= i 2023))))
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.QuantifierEliminationTest.checkLogicalEquivalence(QuantifierEliminationTest.java:368)
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.QuantifierEliminationTest.runQuantifierEliminationTest(QuantifierEliminationTest.java:345)
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.QuantifierEliminationTest.avdiivkaSimplified(QuantifierEliminationTest.java:429)
Standard out
[INFO]: No working directory specified, using /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3
[INFO]: Starting monitored process 283 with /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:1000 -memory:2024 -smt2 -in (exit command is (exit), workingDir is null)
[INFO]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:1000 -memory:2024 -smt2 -in (283)] Waiting until timeout for monitored process
[INFO]: Elimination output: (and (= i 1048) (exists ((i Int)) (and (forall ((k Int)) (or (= 42 (select a k)) (< i (+ k 1)))) (<= i 2023))))
[INFO]: [MP /storage/jenkins/workspace/Ultimate_Ultimate_Nightly_PR-770/releaseScripts/default/adds/z3 SMTLIB2_COMPLIANT=true -t:1000 -memory:2024 -smt2 -in (283)] Ended with exit code 0
de.uni_freiburg.informatik.ultimate.util.MonitoredProcessTest.testProcessToolchainTimeout
Process is still running
Stack trace
java.lang.AssertionError: Process is still running
at de.uni_freiburg.informatik.ultimate.util.MonitoredProcessTest.testProcessToolchainTimeout(MonitoredProcessTest.java:106)
Standard out
[INFO]: No working directory specified, using /usr/bin/sleep
[INFO]: Starting monitored process 3 with /usr/bin/sleep 300 (exit command is null, workingDir is null)
[DEBUG]: [MP /usr/bin/sleep 300 (3)] Finished thread setup
system.SystemTest.initializationError
URI scheme is not "file"
Stack trace
java.lang.IllegalArgumentException: URI scheme is not "file"
at system.SystemTest.testFiles(SystemTest.java:107)
de.uni_freiburg.informatik.ultimate.plugins.spaceex.automata.hybridsystem.ParallelCompositionGeneratorTest.testComputeParallelComposition
expected:<...2) === (); {} ===> ([3), (2) === (); {} ===> (4]), (4) === (); {} ==...> but was:<...2) === (); {} ===> ([4), (2) === (); {} ===> (3]), (4) === (); {} ==...>
Stack trace
org.junit.ComparisonFailure: expected:<...2) === (); {} ===> ([3), (2) === (); {} ===> (4]), (4) === (); {} ==...> but was:<...2) === (); {} ===> ([4), (2) === (); {} ===> (3]), (4) === (); {} ==...>
at de.uni_freiburg.informatik.ultimate.plugins.spaceex.automata.hybridsystem.ParallelCompositionGeneratorTest.testComputeParallelComposition(ParallelCompositionGeneratorTest.java:105)
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.lookupUsingOSGiServiceLoader(ServiceLoaderUtil.java:60)
at jakarta.xml.bind.ContextFinder.find(ContextFinder.java:378)
at jakarta.xml.bind.JAXBContext.newInstance(JAXBContext.java:605)
at jakarta.xml.bind.JAXBContext.newInstance(JAXBContext.java:546)
at de.uni_freiburg.informatik.ultimate.plugins.spaceex.automata.hybridsystem.ParallelCompositionGeneratorTest.testComputeParallelComposition(ParallelCompositionGeneratorTest.java:40)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:59)
at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:56)
at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
at org.junit.runners.ParentRunner$3.evaluate(ParentRunner.java:306)
at org.junit.runners.BlockJUnit4ClassRunner$1.evaluate(BlockJUnit4ClassRunner.java:100)
at org.junit.runners.ParentRunner.runLeaf(ParentRunner.java:366)
at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:103)
at org.junit.runners.BlockJUnit4ClassRunner.runChild(BlockJUnit4ClassRunner.java:63)
at org.junit.runners.ParentRunner$4.run(ParentRunner.java:331)
at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:79)
at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:329)
at org.junit.runners.ParentRunner.access$100(ParentRunner.java:66)
at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:293)
at org.junit.runners.ParentRunner$3.evaluate(ParentRunner.java:306)
at org.junit.runners.ParentRunner.run(ParentRunner.java:413)
at org.junit.runners.Suite.runChild(Suite.java:128)
at org.junit.runners.Suite.runChild(Suite.java:27)
at org.junit.runners.ParentRunner$4.run(ParentRunner.java:331)
at org.junit.runners.ParentRunner$1.schedule(ParentRunner.java:79)
at org.junit.runners.ParentRunner.runChildren(ParentRunner.java:329)
at org.junit.runners.ParentRunner.access$100(ParentRunner.java:66)
at org.junit.runners.ParentRunner$2.evaluate(ParentRunner.java:293)
at org.junit.runners.ParentRunner$3.evaluate(ParentRunner.java:306)
at org.junit.runners.ParentRunner.run(ParentRunner.java:413)
at org.apache.maven.surefire.junitcore.JUnitCore.run(JUnitCore.java:49)
at org.apache.maven.surefire.junitcore.JUnitCoreWrapper.createRequestAndRun(JUnitCoreWrapper.java:120)
at org.apache.maven.surefire.junitcore.JUnitCoreWrapper.executeEager(JUnitCoreWrapper.java:95)
at org.apache.maven.surefire.junitcore.JUnitCoreWrapper.execute(JUnitCoreWrapper.java:75)
at org.apache.maven.surefire.junitcore.JUnitCoreWrapper.execute(JUnitCoreWrapper.java:69)
at org.apache.maven.surefire.junitcore.JUnitCoreProvider.invoke(JUnitCoreProvider.java:146)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at org.apache.maven.surefire.api.util.ReflectionUtils.invokeMethodWithArray2(ReflectionUtils.java:137)
at org.apache.maven.surefire.booter.ProviderFactory$ProviderProxy.invoke(ProviderFactory.java:148)
at org.apache.maven.surefire.booter.ProviderFactory.invokeProvider(ProviderFactory.java:88)
at org.eclipse.tycho.surefire.osgibooter.OsgiSurefireBooter.invokeSureFire(OsgiSurefireBooter.java:195)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at org.eclipse.tycho.surefire.osgibooter.OsgiSurefireBooter.run(OsgiSurefireBooter.java:116)
at org.eclipse.tycho.surefire.osgibooter.HeadlessTestApplication.start(HeadlessTestApplication.java:29)
at org.eclipse.equinox.internal.app.EclipseAppHandle.run(EclipseAppHandle.java:219)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.runApplication(EclipseAppLauncher.java:149)
at org.eclipse.core.runtime.internal.adaptor.EclipseAppLauncher.start(EclipseAppLauncher.java:115)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:467)
at org.eclipse.core.runtime.adaptor.EclipseStarter.run(EclipseStarter.java:298)
at java.base/jdk.internal.reflect.DirectMethodHandleAccessor.invoke(DirectMethodHandleAccessor.java:103)
at java.base/java.lang.reflect.Method.invoke(Method.java:580)
at org.eclipse.equinox.launcher.Main.invokeFramework(Main.java:627)
at org.eclipse.equinox.launcher.Main.basicRun(Main.java:575)
at org.eclipse.equinox.launcher.Main.run(Main.java:1431)
at org.eclipse.equinox.launcher.Main.main(Main.java:1403)
Standard out
Starting Test 1..
[DEBUG]: creating hybridsystem for system: sys1
[DEBUG]: Added parameter x
[DEBUG]: Added parameter y
[DEBUG]: Added parameter x
[DEBUG]: [sys1.aut1_1]: Added location: loc1(1), Invariant: x <= 10, Flow: x == 10, IsForbidden?: false
[DEBUG]: BINDS {sys1.aut1_1={x=x}}
[DEBUG]: Added parameter y
[DEBUG]: [sys1.aut2_1]: Added location: loc1(1), Invariant: y <= 10, Flow: y == 10, IsForbidden?: false
[DEBUG]: BINDS {sys1.aut1_1={x=x}, sys1.aut2_1={y=y}}
[DEBUG]: hybridsystem created:
System sys1:
Parameters (global):
* x
* y
Parameters (local):
Constants (global):
Constants (local):
Labels:
Automata:
Automaton sys1.aut1_1:
sys1.aut1_1:
parameters: [x][]
constants: [][]
labels: []
locations: {1=loc1(1), Invariant: x <= 10, Flow: x == 10, IsForbidden?: false}
initial Location: {}
transitions: []
Automaton sys1.aut2_1:
sys1.aut2_1:
parameters: [y][]
constants: [][]
labels: []
locations: {1=loc1(1), Invariant: y <= 10, Flow: y == 10, IsForbidden?: false}
initial Location: {}
transitions: []
Subsystems:
binds:
automata: sys1.aut1_1 bind: {x=x}
automata: sys1.aut2_1 bind: {y=y}
[DEBUG]: ####################### STARTING PARALLEL COMPOSITION ###########################
[DEBUG]: ###################### STACK UPDATE #########################
[DEBUG]: *loc1(1), Invariant: x <= 10, Flow: x == 10, IsForbidden?: false
[DEBUG]: *loc1(1), Invariant: y <= 10, Flow: y == 10, IsForbidden?: false
[DEBUG]: ##################### STACK UPDATE END #######################
[DEBUG]: CURRENT NODE:loc_loc1_loc1_
[DEBUG]: ############### ADDING SET TO VISITED ################
[DEBUG]: *loc1(1), Invariant: x <= 10, Flow: x == 10, IsForbidden?: false
[DEBUG]: *loc1(1), Invariant: y <= 10, Flow: y == 10, IsForbidden?: false
[DEBUG]: ###########################################
[DEBUG]: ############### OUTGOING TRANSITIONS ###############
[DEBUG]: #####################################################
[DEBUG]: ####################### PARALLEL COMPOSITION END ###########################
MERGE0:
parameters: [][x, y]
constants: [][]
labels: []
locations: {1=loc_loc1_loc1_(1), Invariant: x <= 10 & y <= 10, Flow: x == 10 & y == 10, IsForbidden?: false}
initial Location: {}
transitions: []
Done in 519.7237 milliseconds
Starting Test 2..
[DEBUG]: creating hybridsystem for system: sys1
[DEBUG]: Added parameter x
[DEBUG]: Added parameter y
[DEBUG]: Added parameter x
[DEBUG]: [sys1.aut1_1]: Added location: loc1(1), Invariant: x <= 10, Flow: x == 10, IsForbidden?: false
[DEBUG]: BINDS {sys1.aut1_1={x=x}}
[DEBUG]: Added parameter y
[DEBUG]: [sys1.aut2_1]: Added location: loc1(1), Invariant: y <= 10, Flow: y == 10, IsForbidden?: false
[DEBUG]: [sys1.aut2_1]: Added location: loc2(2), Invariant: , Flow: , IsForbidden?: false
[DEBUG]: [sys1.aut2_1]: Added transition: (1) === (); {} ===> (2)
[DEBUG]: BINDS {sys1.aut1_1={x=x}, sys1.aut2_1={y=y}}
[DEBUG]: hybridsystem created:
System sys1:
Parameters (global):
* x
* y
Parameters (local):
Constants (global):
Constants (local):
Labels:
Automata:
Automaton sys1.aut1_1:
sys1.aut1_1:
parameters: [x][]
constants: [][]
labels: []
locations: {1=loc1(1), Invariant: x <= 10, Flow: x == 10, IsForbidden?: false}
initial Location: {}
transitions: []
Automaton sys1.aut2_1:
sys1.aut2_1:
parameters: [y][]
constants: [][]
labels: []
locations: {1=loc1(1), Invariant: y <= 10, Flow: y == 10, IsForbidden?: false, 2=loc2(2), Invariant: , Flow: , IsForbidden?: false}
initial Location: {}
transitions: [(1) === (); {} ===> (2)]
Subsystems:
binds:
automata: sys1.aut1_1 bind: {x=x}
automata: sys1.aut2_1 bind: {y=y}
[DEBUG]: ####################### STARTING PARALLEL COMPOSITION ###########################
[DEBUG]: ###################### STACK UPDATE #########################
[DEBUG]: *loc1(1), Invariant: x <= 10, Flow: x == 10, IsForbidden?: false
[DEBUG]: *loc1(1), Invariant: y <= 10, Flow: y == 10, IsForbidden?: false
[DEBUG]: ##################### STACK UPDATE END #######################
[DEBUG]: CURRENT NODE:loc_loc1_loc1_
[DEBUG]: ############### ADDING SET TO VISITED ################
[DEBUG]: *loc1(1), Invariant: x <= 10, Flow: x == 10, IsForbidden?: false
[DEBUG]: *loc1(1), Invariant: y <= 10, Flow: y == 10, IsForbidden?: false
[DEBUG]: ###########################################
[DEBUG]: ############### OUTGOING TRANSITIONS ###############
[DEBUG]: *(1) === (); {} ===> (2)
[DEBUG]: #####################################################
[DEBUG]: ###################### STACK UPDATE #########################
[DEBUG]: *loc2(2), Invariant: , Flow: , IsForbidden?: false
[DEBUG]: *loc1(1), Invariant: x <= 10, Flow: x == 10, IsForbidden?: false
[DEBUG]: ##################### STACK UPDATE END #######################
[DEBUG]: ################## CURRENT TARGETS #####################
[DEBUG]: TARGET LOCATION:loc_loc2_loc1_
[DEBUG]: TRANSITION INFO: [, , ]
[DEBUG]: ################## CURRENT TARGETS END #################
[DEBUG]: CURRENT NODE:loc_loc2_loc1_
[DEBUG]: ############### ADDING SET TO VISITED ################
[DEBUG]: *loc2(2), Invariant: , Flow: , IsForbidden?: false
[DEBUG]: *loc1(1), Invariant: x <= 10, Flow: x == 10, IsForbidden?: false
[DEBUG]: ###########################################
[DEBUG]: ############### OUTGOING TRANSITIONS ###############
[DEBUG]: #####################################################
[DEBUG]: ####################### PARALLEL COMPOSITION END ###########################
MERGE0:
parameters: [][x, y]
constants: [][]
labels: []
locations: {1=loc_loc1_loc1_(1), Invariant: x <= 10 & y <= 10, Flow: x == 10 & y == 10, IsForbidden?: false, 2=loc_loc2_loc1_(2), Invariant: x <= 10, Flow: x == 10, IsForbidden?: false}
initial Location: {}
transitions: [(1) === (); {} ===> (2)]
Done in 9.965724 milliseconds
Starting Test 3..
[DEBUG]: creating hybridsystem for system: sys1
[DEBUG]: Added parameter x
[DEBUG]: Added parameter jump1
[DEBUG]: Added parameter y
[DEBUG]: Added parameter x
[DEBUG]: Added parameter jump1
[DEBUG]: [sys1.aut1_1]: Added location: loc1(1), Invariant: x <= 4, Flow: x==1, IsForbidden?: false
[DEBUG]: [sys1.aut1_1]: Added location: loc2(2), Invariant: x <= 5, Flow: x==1, IsForbidden?: false
[DEBUG]: [sys1.aut1_1]: Added location: loc3(3), Invariant: x <= 6, Flow: x==1, IsForbidden?: false
[DEBUG]: [sys1.aut1_1]: Added transition: (1) === (); {x==0}; Label: jump1 ===> (2)
[DEBUG]: [sys1.aut1_1]: Added transition: (2) === (); {} ===> (3)
[DEBUG]: BINDS {sys1.aut1_1={x=x, jump1=jump1}}
[DEBUG]: Added parameter y
[DEBUG]: Added parameter jump1
[DEBUG]: [sys1.aut2_1]: Added location: loc1(1), Invariant: y <= 4, Flow: y==1, IsForbidden?: false
[DEBUG]: [sys1.aut2_1]: Added location: loc2(2), Invariant: y <= 5, Flow: y==1, IsForbidden?: false
[DEBUG]: [sys1.aut2_1]: Added location: loc3(3), Invariant: y <= 6, Flow: y==1, IsForbidden?: false
[DEBUG]: [sys1.aut2_1]: Added transition: (1) === (); {y==0}; Label: jump1 ===> (2)
[DEBUG]: [sys1.aut2_1]: Added transition: (2) === (); {} ===> (3)
[DEBUG]: BINDS {sys1.aut1_1={x=x, jump1=jump1}, sys1.aut2_1={y=y, jump1=jump1}}
[DEBUG]: hybridsystem created:
System sys1:
Parameters (global):
* x
* y
Parameters (local):
Constants (global):
Constants (local):
Labels:
* jump1
Automata:
Automaton sys1.aut1_1:
sys1.aut1_1:
parameters: [x][]
constants: [][]
labels: [jump1]
locations: {1=loc1(1), Invariant: x <= 4, Flow: x==1, IsForbidden?: false, 2=loc2(2), Invariant: x <= 5, Flow: x==1, IsForbidden?: false, 3=loc3(3), Invariant: x <= 6, Flow: x==1, IsForbidden?: false}
initial Location: {}
transitions: [(1) === (); {x==0}; Label: jump1 ===> (2), (2) === (); {} ===> (3)]
Automaton sys1.aut2_1:
sys1.aut2_1:
parameters: [y][]
constants: [][]
labels: [jump1]
locations: {1=loc1(1), Invariant: y <= 4, Flow: y==1, IsForbidden?: false, 2=loc2(2), Invariant: y <= 5, Flow: y==1, IsForbidden?: false, 3=loc3(3), Invariant: y <= 6, Flow: y==1, IsForbidden?: false}
initial Location: {}
transitions: [(1) === (); {y==0}; Label: jump1 ===> (2), (2) === (); {} ===> (3)]
Subsystems:
binds:
automata: sys1.aut1_1 bind: {x=x, jump1=jump1}
automata: sys1.aut2_1 bind: {y=y, jump1=jump1}
[DEBUG]: ####################### STARTING PARALLEL COMPOSITION ###########################
[DEBUG]: ###################### STACK UPDATE #########################
[DEBUG]: *loc1(1), Invariant: x <= 4, Flow: x==1, IsForbidden?: false
[DEBUG]: *loc1(1), Invariant: y <= 4, Flow: y==1, IsForbidden?: false
[DEBUG]: ##################### STACK UPDATE END #######################
[DEBUG]: CURRENT NODE:loc_loc1_loc1_
[DEBUG]: ############### ADDING SET TO VISITED ################
[DEBUG]: *loc1(1), Invariant: x <= 4, Flow: x==1, IsForbidden?: false
[DEBUG]: *loc1(1), Invariant: y <= 4, Flow: y==1, IsForbidden?: false
[DEBUG]: ###########################################
[DEBUG]: ############### OUTGOING TRANSITIONS ###############
[DEBUG]: *(1) === (); {x==0}; Label: jump1 ===> (2)
[DEBUG]: *(1) === (); {y==0}; Label: jump1 ===> (2)
[DEBUG]: #####################################################
[DEBUG]: ###################### STACK UPDATE #########################
[DEBUG]: *loc2(2), Invariant: x <= 5, Flow: x==1, IsForbidden?: false
[DEBUG]: *loc2(2), Invariant: y <= 5, Flow: y==1, IsForbidden?: false
[DEBUG]: ##################### STACK UPDATE END #######################
[DEBUG]: ################## CURRENT TARGETS #####################
[DEBUG]: TARGET LOCATION:loc_loc2_loc2_
[DEBUG]: TRANSITION INFO: [jump1, , x==0 & y==0]
[DEBUG]: ################## CURRENT TARGETS END #################
[DEBUG]: CURRENT NODE:loc_loc2_loc2_
[DEBUG]: ############### ADDING SET TO VISITED ################
[DEBUG]: *loc2(2), Invariant: x <= 5, Flow: x==1, IsForbidden?: false
[DEBUG]: *loc2(2), Invariant: y <= 5, Flow: y==1, IsForbidden?: false
[DEBUG]: ###########################################
[DEBUG]: ############### OUTGOING TRANSITIONS ###############
[DEBUG]: *(2) === (); {} ===> (3)
[DEBUG]: *(2) === (); {} ===> (3)
[DEBUG]: #####################################################
[DEBUG]: ###################### STACK UPDATE #########################
[DEBUG]: *loc3(3), Invariant: x <= 6, Flow: x==1, IsForbidden?: false
[DEBUG]: *loc2(2), Invariant: y <= 5, Flow: y==1, IsForbidden?: false
[DEBUG]: ##################### STACK UPDATE END #######################
[DEBUG]: ###################### STACK UPDATE #########################
[DEBUG]: *loc2(2), Invariant: x <= 5, Flow: x==1, IsForbidden?: false
[DEBUG]: *loc3(3), Invariant: y <= 6, Flow: y==1, IsForbidden?: false
[DEBUG]: ##################### STACK UPDATE END #######################
[DEBUG]: ################## CURRENT TARGETS #####################
[DEBUG]: TARGET LOCATION:loc_loc2_loc3_
[DEBUG]: TRANSITION INFO: [, , ]
[DEBUG]: TARGET LOCATION:loc_loc3_loc2_
[DEBUG]: TRANSITION INFO: [, , ]
[DEBUG]: ################## CURRENT TARGETS END #################
[DEBUG]: CURRENT NODE:loc_loc2_loc3_
[DEBUG]: ############### ADDING SET TO VISITED ################
[DEBUG]: *loc2(2), Invariant: x <= 5, Flow: x==1, IsForbidden?: false
[DEBUG]: *loc3(3), Invariant: y <= 6, Flow: y==1, IsForbidden?: false
[DEBUG]: ###########################################
[DEBUG]: ############### OUTGOING TRANSITIONS ###############
[DEBUG]: *(2) === (); {} ===> (3)
[DEBUG]: #####################################################
[DEBUG]: ###################### STACK UPDATE #########################
[DEBUG]: *loc3(3), Invariant: x <= 6, Flow: x==1, IsForbidden?: false
[DEBUG]: *loc3(3), Invariant: y <= 6, Flow: y==1, IsForbidden?: false
[DEBUG]: ##################### STACK UPDATE END #######################
[DEBUG]: ################## CURRENT TARGETS #####################
[DEBUG]: TARGET LOCATION:loc_loc3_loc3_
[DEBUG]: TRANSITION INFO: [, , ]
[DEBUG]: ################## CURRENT TARGETS END #################
[DEBUG]: CURRENT NODE:loc_loc3_loc3_
[DEBUG]: ############### ADDING SET TO VISITED ################
[DEBUG]: *loc3(3), Invariant: x <= 6, Flow: x==1, IsForbidden?: false
[DEBUG]: *loc3(3), Invariant: y <= 6, Flow: y==1, IsForbidden?: false
[DEBUG]: ###########################################
[DEBUG]: ############### OUTGOING TRANSITIONS ###############
[DEBUG]: #####################################################
[DEBUG]: CURRENT NODE:loc_loc3_loc2_
[DEBUG]: ############### ADDING SET TO VISITED ################
[DEBUG]: *loc3(3), Invariant: x <= 6, Flow: x==1, IsForbidden?: false
[DEBUG]: *loc2(2), Invariant: y <= 5, Flow: y==1, IsForbidden?: false
[DEBUG]: ###########################################
[DEBUG]: ############### OUTGOING TRANSITIONS ###############
[DEBUG]: *(2) === (); {} ===> (3)
[DEBUG]: #####################################################
[DEBUG]: ###################### STACK UPDATE #########################
[DEBUG]: *loc3(3), Invariant: y <= 6, Flow: y==1, IsForbidden?: false
[DEBUG]: *loc3(3), Invariant: x <= 6, Flow: x==1, IsForbidden?: false
[DEBUG]: ##################### STACK UPDATE END #######################
[DEBUG]: ################## CURRENT TARGETS #####################
[DEBUG]: TARGET LOCATION:loc_loc3_loc3_
[DEBUG]: TRANSITION INFO: [, , ]
[DEBUG]: ################## CURRENT TARGETS END #################
[DEBUG]: ####################### PARALLEL COMPOSITION END ###########################
MERGE0:
parameters: [][x, y]
constants: [][]
labels: [jump1]
locations: {1=loc_loc1_loc1_(1), Invariant: x <= 4 & y <= 4, Flow: x==1 & y==1, IsForbidden?: false, 2=loc_loc2_loc2_(2), Invariant: x <= 5 & y <= 5, Flow: x==1 & y==1, IsForbidden?: false, 3=loc_loc3_loc2_(3), Invariant: x <= 6 & y <= 5, Flow: x==1 & y==1, IsForbidden?: false, 4=loc_loc2_loc3_(4), Invariant: x <= 5 & y <= 6, Flow: x==1 & y==1, IsForbidden?: false, 5=loc_loc3_loc3_(5), Invariant: x <= 6 & y <= 6, Flow: x==1 & y==1, IsForbidden?: false}
initial Location: {}
transitions: [(1) === (); {x==0 & y==0}; Label: jump1 ===> (2), (2) === (); {} ===> (4), (2) === (); {} ===> (3), (4) === (); {} ===> (5), (3) === (); {} ===> (5)]
more test results are not shown here, view them on Jenkins
Loading