TestLocalSymbols

2

tests

0

failures

0

ignored

7.633s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 7.588s passed
testSkolemization() 0.045s passed

Standard output

119927     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
119927     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
119942     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
119942     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
119942     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
119942     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
119942     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
119942     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
119942     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
119942     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
119942     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
119942     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
119958     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
119958     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
120146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
120146     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 480.3ns 
120146     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
120552     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
120552     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
120552     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
120552     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
122272     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
126993     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.66s 
127134     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
127247     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 34.1ns 
127453     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
127484     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
127531     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''