TestLocalSymbols

2

tests

0

failures

0

ignored

6.547s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 6.501s passed
testSkolemization() 0.046s passed

Standard output

124036     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
124037     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
124039     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124039     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124039     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
124039     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124039     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124039     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
124039     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
124039     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124054     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124054     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
124054     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124054     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124070     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
124070     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 408ns 
124085     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124508     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
124508     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
124508     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
124508     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
125727     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
130219     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.14s 
130281     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
130393     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36ns 
130506     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 2, command: 'rule orRight' 
130553     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'' 
130553     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''