TestProofScriptCommand
|
100%
successful |
Tests
Test | Method name | Duration | Result |
---|---|---|---|
[1] unhide.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/unhide.props | testProofScript(String, Path)[1] | 3.127s | passed |
[2] selectFormula.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/selectFormula.props | testProofScript(String, Path)[2] | 3.190s | passed |
[3] hide.exc.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/hide.exc.props | testProofScript(String, Path)[3] | 3.256s | passed |
[4] unhide2.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/unhide2.props | testProofScript(String, Path)[4] | 3.136s | passed |
[5] rule.exc.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/rule.exc.props | testProofScript(String, Path)[5] | 3.080s | passed |
[6] andRight.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/andRight.props | testProofScript(String, Path)[6] | 3.110s | passed |
[7] hide.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/hide.props | testProofScript(String, Path)[7] | 3.041s | passed |
Standard output
179865 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/proofscript_key_unhide.props13208912171354064256.key 179865 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.79ms 179866 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 182937 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.07s 182959 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_unhide.props13208912171354064256.key 182964 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 182966 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'rule impRight' on goal 0 (script from line 1) 182969 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'hide '2=3 ==> 3=4'' on goal 1 (script from line 2) 182971 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'unhide '2=3 ==>'' on goal 3 (script from line 3) 182975 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 4: 'unhide '==> 3=4'' on goal 4 (script from line 4) 182988 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/proofscript_key_selectFormula.props16769685432440455779.key 182988 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 509.52ns 182989 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 186145 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.16s 186166 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_selectFormula.props16769685432440455779.key 186167 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.2ns 186168 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 1) 186174 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'select formula="b"' on goal 3 (script from line 2) 186177 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/proofscript_key_hide.exc.props17458356819498568848.key 186177 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 93.9ns 186178 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 189398 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.22s 189421 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_hide.exc.props17458356819498568848.key 189424 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.7ns 189425 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 1) 189429 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'hide "b ==>"' on goal 1 (script from line 2) 189430 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine GOALS: 1 189431 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine [a]==>[b] 189434 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/proofscript_key_unhide2.props15751097627015703403.key 189434 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 447.92ns 189436 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 192538 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.1s 192560 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_unhide2.props15751097627015703403.key 192562 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 192563 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'rule impRight' on goal 0 (script from line 1) 192565 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'hide '2=3 ==> 3=4'' on goal 1 (script from line 2) 192566 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 3: 'unhide '2=3 ==> 3=4'' on goal 3 (script from line 3) 192570 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/proofscript_key_rule.exc.props2551753523219466770.key 192570 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 428.42ns 192571 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 195624 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.05s 195645 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_rule.exc.props2551753523219466770.key 195647 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.5ns 195647 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'rule andLeft' on goal 0 (script from line 1) 195648 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine GOALS: 1 195648 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine []==>[and(a,b)] 195650 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/proofscript_key_andRight.props3945233367056889188.key 195650 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 109.4ns 195651 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 198736 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.08s 198755 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_andRight.props3945233367056889188.key 198756 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.9ns 198757 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'rule andRight' on goal 0 (script from line 1) 198760 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/proofscript_key_hide.props11427324356083030386.key 198760 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Environment load took 97.1ns 198761 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Creating init config 201770 DEBUG Test worker d.u.i.k.p.i.AbstractProblemLoader Init config took 3.01s 201788 INFO Test worker d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_hide.props11427324356083030386.key 201790 DEBUG Test worker d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 201790 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 1: 'macro split-prop' on goal 0 (script from line 1) 201797 DEBUG Test worker d.u.i.k.m.s.ProofScriptEngine 2: 'hide "a ==> d, e"' on goal 5 (script from line 2)