TestProofScriptCommand

all > de.uka.ilkd.key.macros.scripts > TestProofScriptCommand
7

tests
0

failures
0

ignored
3.029s

duration
100%

successful

Tests

Test Method name Duration Result
[1] andRight.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\andRight.props testProofScript(String, Path)[1] 0.373s passed
[2] hide.exc.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\hide.exc.props testProofScript(String, Path)[2] 0.416s passed
[3] hide.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\hide.props testProofScript(String, Path)[3] 0.345s passed
[4] rule.exc.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\rule.exc.props testProofScript(String, Path)[4] 0.762s passed
[5] selectFormula.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\selectFormula.props testProofScript(String, Path)[5] 0.332s passed
[6] unhide.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\unhide.props testProofScript(String, Path)[6] 0.475s passed
[7] unhide2.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\unhide2.props testProofScript(String, Path)[7] 0.326s passed

Standard error

95750      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\proofscript_key_andRight.props12867344627965847009.key 
95750      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 290.3ns 
95750      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
95911      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
95942      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
95942      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
95942      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
95942      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
95942      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
95942      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
95978      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
95980      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
96011      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
96042      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 296.52ms 
96073      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_andRight.props12867344627965847009.key 
96105      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 10.1ns 
96105      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'rule andRight' 
96120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\proofscript_key_hide.exc.props15442484327745034167.key 
96120      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.1ns 
96120      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96336      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
96383      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
96383      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
96383      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
96383      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
96383      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
96383      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
96399      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
96399      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
96430      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
96492      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 372.98ms 
96524      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_hide.exc.props15442484327745034167.key 
96524      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
96524      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'macro split-prop' 
96539      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 1, source line: 2, command: 'hide "b ==>"' 
96539      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine GOALS: 1 
96539      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [a]==>[b] 
96539      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\proofscript_key_hide.props13362202458514347603.key 
96539      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 122.9ns 
96539      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
96674      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
96705      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
96705      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
96705      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
96705      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
96705      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
96721      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
96737      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
96737      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
96768      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
96830      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 296.02ms 
96862      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_hide.props13362202458514347603.key 
96862      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.2ns 
96862      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'macro split-prop' 
96877      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 5, source line: 2, command: 'hide "a ==> d, e"' 
97259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\proofscript_key_rule.exc.props4096873659130923599.key 
97259      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 175.3ns 
97259      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97447      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
97494      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
97494      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
97494      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
97494      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
97494      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
97494      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
97549      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
97549      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
97580      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
97611      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 353.46ms 
97643      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_rule.exc.props4096873659130923599.key 
97643      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.2ns 
97643      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'rule andLeft' 
97643      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine GOALS: 1 
97643      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine []==>[and(a,b)] 
97643      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\proofscript_key_selectFormula.props6835607002630595844.key 
97643      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 123.5ns 
97643      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
97779      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
97841      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
97841      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
97841      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
97841      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
97841      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
97857      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
97872      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
97872      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
97904      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
97935      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 289.4ms 
97950      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_selectFormula.props6835607002630595844.key 
97966      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.9ns 
97966      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'macro split-prop' 
97982      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 2, command: 'select formula="b"' 
97982      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\proofscript_key_unhide.props6876759244664489056.key 
97982      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 132.7ns 
97982      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98171      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
98218      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
98233      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
98233      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
98233      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
98233      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
98233      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
98265      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
98265      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
98296      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
98343      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 357.98ms 
98437      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_unhide.props6876759244664489056.key 
98437      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.4ns 
98437      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'rule impRight' 
98437      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 1, source line: 2, command: 'hide '2=3 ==> 3=4'' 
98453      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 3, source line: 3, command: 'unhide '2=3 ==>'' 
98453      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 4, source line: 4, command: 'unhide '==> 3=4'' 
98453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from C:\Users\RUNNER~1\AppData\Local\Temp\proofscript_key_unhide2.props7359653997777666026.key 
98453      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.04ms 
98453      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98627      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
98658      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
98658      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
98658      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
98658      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
98658      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
98658      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
98689      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
98689      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
98705      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
98752      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 290.2ms 
98768      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_unhide2.props7359653997777666026.key 
98768      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.3ns 
98768      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'rule impRight' 
98768      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 1, source line: 2, command: 'hide '2=3 ==> 3=4'' 
98768      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 3, source line: 3, command: 'unhide '2=3 ==> 3=4''