TestLocalSymbols

2

tests

0

failures

0

ignored

11.212s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 11.127s passed
testSkolemization() 0.085s passed

Standard output

164778     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
164778     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
164778     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
164778     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
164778     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
164778     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
164778     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
164794     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
164794     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
164794     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
164794     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
164794     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
164810     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
164810     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
165706     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
165706     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 778.1ns 
165721     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
166331     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
166331     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
166331     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
166331     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
168624     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
175227     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 9.39s 
175305     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
175445     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.7ns 
175753     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 2, command: 'rule orRight' 
175964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 1, source line: 3, command: 'rule allRight formula='\forall int i; i > 0'' 
175964     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 2, source line: 4, command: 'rule allRight formula='\forall int i; i < 0''