EndToEndTests

11

tests

0

failures

0

ignored

4m6.69s

duration

100%

successful

Tests

Test Duration Result
deduplicateChecksMergabilityCorrectly() 9.158s passed
sliceAgatha() 8.590s passed
sliceAgathaWithOpenGoal() 8.631s passed
sliceCutExample() 8.761s passed
sliceDuplicatesAway() 36.059s passed
sliceDuplicatesAwayOpenGoals() 35.965s passed
sliceIfThenElseSplit() 47.303s passed
sliceRemoveDuplicates() 53.008s passed
sliceSimpleSMT() 0.001s passed
sliceSitaRearrange() 22.393s passed
sliceWithOpenGoal() 16.816s passed

Standard output

loading /home/runner/work/key/key/keyext.slicing/src/test/resources/testcase/sitaRearrange.zproof
[14:44:04.037] ?[31mWARN ?[0;39m ?[36mProofIndependentSettings?[0;39m - The settings in /home/runner/.key/proofIndependentSettings.props are *not* read due to flag 'key.disregardSettings'
[14:44:04.213] ?[31mWARN ?[0;39m ?[36mProofSettings?[0;39m - The settings in /home/runner/.key/proof-settings.props are *not* read.
[14:44:16.761] ?[34mINFO ?[0;39m ?[36mKeyStrokeSettings?[0;39m - Save keyboard shortcuts to: /home/runner/.key/keystrokes.properties
loading /home/runner/work/key/key/keyext.slicing/src/test/resources/testcase/ifThenElseSplit.proof
loading /home/runner/work/key/key/keyext.slicing/src/test/resources/testcase/ifThenElseSplit.proof
[14:44:39.444] ?[34mINFO ?[0;39m ?[36mDependencyAnalyzer?[0;39m - merging 2 and 3
loading /tmp/KeYslice7673176963554736162/ifThenElseSplit_slice1.proof
[14:44:49.050] ?[34mINFO ?[0;39m ?[36mDependencyAnalyzer?[0;39m - merging 3 and 4
loading /tmp/KeYslice12747104037877306986/ifThenElseSplit_slice2.proof
[14:44:58.078] ?[34mINFO ?[0;39m ?[36mDependencyAnalyzer?[0;39m - merging 4 and 5
loading /tmp/KeYslice16638883032597536725/ifThenElseSplit_slice3.proof
[14:45:07.444] ?[34mINFO ?[0;39m ?[36mDependencyAnalyzer?[0;39m - merging 5 and 6
loading /home/runner/work/key/key/keyext.slicing/src/test/resources/testcase/deduplicateCheck4.proof
loading /home/runner/work/key/key/keyext.slicing/src/test/resources/testcase/exampleDuplicate.proof
[14:45:25.834] ?[34mINFO ?[0;39m ?[36mDependencyAnalyzer?[0;39m - merging 2 and 3
loading /tmp/KeYslice15614499335034531578/exampleDuplicate_slice1.proof
[14:45:34.960] ?[34mINFO ?[0;39m ?[36mDependencyAnalyzer?[0;39m - merging 3 and 4
loading /tmp/KeYslice17916563306228334972/exampleDuplicate_slice2.proof
[14:45:43.751] ?[34mINFO ?[0;39m ?[36mDependencyAnalyzer?[0;39m - merging 4 and 5
loading /tmp/KeYslice2816696381643337638/exampleDuplicate_slice3.proof
loading /home/runner/work/key/key/keyext.slicing/src/test/resources/testcase/exampleDuplicateOpen.proof
[14:46:01.680] ?[34mINFO ?[0;39m ?[36mDependencyAnalyzer?[0;39m - merging 2 and 3
loading /tmp/KeYslice18252084685939936586/exampleDuplicateOpen_slice1.proof
[14:46:10.782] ?[34mINFO ?[0;39m ?[36mDependencyAnalyzer?[0;39m - merging 3 and 4
loading /tmp/KeYslice15136906267512878102/exampleDuplicateOpen_slice2.proof
[14:46:19.736] ?[34mINFO ?[0;39m ?[36mDependencyAnalyzer?[0;39m - merging 4 and 5
loading /tmp/KeYslice10450250042139489346/exampleDuplicateOpen_slice3.proof
loading /home/runner/work/key/key/keyext.slicing/src/test/resources/testcase/cutExample.proof
loading /home/runner/work/key/key/keyext.slicing/src/test/resources/testcase/agathaOpenGoal.proof
loading /home/runner/work/key/key/keyext.slicing/src/test/resources/testcase/openGoal1.proof
loading /home/runner/work/key/key/keyext.slicing/src/test/resources/testcase/openGoal2.proof
loading /home/runner/work/key/key/keyext.slicing/src/test/resources/testcase/agatha.proof
loading /home/runner/work/key/key/keyext.slicing/src/test/resources/testcase/removeDuplicates.zproof
loading /tmp/KeYslice8419554240321151078/RemoveDup(RemoveDup__removeDup((I)).JML normal_behavior operation contract.0_slice1.proof
loading /tmp/KeYslice7310616003463941752/RemoveDup(RemoveDup__removeDup((I)).JML normal_behavior operation contract.0_slice2.proof
loading /tmp/KeYslice5895983410847861554/RemoveDup(RemoveDup__removeDup((I)).JML normal_behavior operation contract.0_slice3.proof