TestLocalSymbols

2

tests

0

failures

0

ignored

6.161s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 6.123s passed
testSkolemization() 0.038s passed

Standard output

100437     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
100437     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
100437     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
100437     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
100437     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
100437     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
100437     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
100437     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
100437     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
100452     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
100452     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
100452     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
100452     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
100452     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
100484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
100484     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 891.8ns 
100484     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
100892     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
100908     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
100908     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
100908     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
102393     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
106316     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.82s 
106378     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
106447     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39.8ns 
106529     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' on goal 0 (script from line 2) 
106562     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' on goal 1 (script from line 3) 
106564     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0'' on goal 2 (script from line 4)