TestProofScriptCommand

7

tests

0

failures

0

ignored

2.385s

duration

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] 0.317s passed
[2] unhide2.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/unhide2.props testProofScript(String, Path)[2] 0.342s passed
[3] 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)[3] 0.386s passed
[4] selectFormula.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/selectFormula.props testProofScript(String, Path)[4] 0.298s passed
[5] hide.props, /home/runner/work/key/key/key.core/build/resources/test/de/uka/ilkd/key/macros/scripts/cases/hide.props testProofScript(String, Path)[5] 0.312s 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] 0.391s passed
[7] 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)[7] 0.339s passed

Standard error

32085      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/proofscript_key_unhide.props4986690884248184278.key 
32085      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.2ns 
32086      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32221      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
32260      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
32262      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
32262      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
32263      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
32264      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
32267      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
32286      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
32290      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
32324      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
32361      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 274.98ms 
32386      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_unhide.props4986690884248184278.key 
32388      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
32389      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'rule impRight' 
32392      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 1, source line: 2, command: 'hide '2=3 ==> 3=4'' 
32393      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 3, source line: 3, command: 'unhide '2=3 ==>'' 
32395      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [4] goal: 4, source line: 4, command: 'unhide '==> 3=4'' 
32402      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/proofscript_key_unhide2.props8664713549953715888.key 
32402      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 91.7ns 
32402      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32568      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
32608      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
32613      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
32614      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
32614      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
32615      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
32618      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
32638      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
32642      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
32676      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
32713      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 310.44ms 
32735      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_unhide2.props8664713549953715888.key 
32737      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
32738      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'rule impRight' 
32741      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 1, source line: 2, command: 'hide '2=3 ==> 3=4'' 
32742      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 3, source line: 3, command: 'unhide '2=3 ==> 3=4'' 
32745      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/proofscript_key_rule.exc.props3639837996086344536.key 
32745      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 70.5ns 
32745      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
32880      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
32919      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
32921      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
32922      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
32922      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
32923      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
32926      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
32945      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
32949      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
33068      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
33105      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 359.76ms 
33125      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_rule.exc.props3639837996086344536.key 
33127      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 7.5ns 
33128      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'rule andLeft' 
33129      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine GOALS: 1 
33129      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine []==>[and(a,b)] 
33131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/proofscript_key_selectFormula.props6600711072088440737.key 
33131      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 68.3ns 
33131      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33257      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
33295      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
33298      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
33298      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
33298      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
33299      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
33303      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
33322      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
33325      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
33359      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
33397      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 265.74ms 
33416      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_selectFormula.props6600711072088440737.key 
33418      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9ns 
33419      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'macro split-prop' 
33427      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 3, source line: 2, command: 'select formula="b"' 
33430      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/proofscript_key_hide.props9498003363847241423.key 
33430      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 85.4ns 
33430      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33563      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
33602      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
33604      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
33604      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
33605      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
33606      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
33609      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
33627      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
33631      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
33665      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
33706      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 275.85ms 
33727      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_hide.props9498003363847241423.key 
33729      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.4ns 
33730      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'macro split-prop' 
33740      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 5, source line: 2, command: 'hide "a ==> d, e"' 
33742      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/proofscript_key_andRight.props15016229095938556713.key 
33742      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 105.9ns 
33743      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
33876      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
33915      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
33917      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
33918      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
33918      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
33920      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
33923      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
33942      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
33946      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
33980      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
34110      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 367.21ms 
34128      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_andRight.props15016229095938556713.key 
34131      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 8.8ns 
34131      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'rule andRight' 
34136      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from /tmp/proofscript_key_hide.exc.props13781286625534388667.key 
34137      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 729.12ns 
34137      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
34283      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: boolean, formerNode: /*@ pure @*/
boolean 
34327      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure*/
int, formerNode: int 
34330      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
int, formerNode: int 
34330      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
boolean, formerNode: /*@ pure @*/
boolean 
34331      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
char, formerNode: char 
34333      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: byte[], formerNode: byte[] 
34337      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@ helper */
java.lang.String, formerNode: java.lang.String 
34359      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@strictly_pure*/
java.lang.String, formerNode: java.lang.String 
34364      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@nullable@*/
Object, formerNode: Object 
34403      ERROR Test worker     d.u.i.k.j.KeYJPMapping    Duplicate registration of node: /*@pure@*/
String, formerNode: String 
34447      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 309.46ms 
34465      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof proofscript_key_hide.exc.props13781286625534388667.key 
34467      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 9.3ns 
34468      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 1, command: 'macro split-prop' 
34472      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 1, source line: 2, command: 'hide "b ==>"' 
34472      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine GOALS: 1 
34473      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [a]==>[b]