TestLocalSymbols

2

tests

0

failures

0

ignored

5.923s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 5.874s passed
testSkolemization() 0.049s passed

Standard output

136113     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
136113     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
136113     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
136113     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
136113     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
136113     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
136113     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
136129     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
136129     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
136129     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
136129     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
136129     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
136129     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
136129     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
136160     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
136191     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.24ms 
136191     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
136645     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
136645     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
136645     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
136645     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
137833     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
141741     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.55s 
141804     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
141882     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 43.9ns 
141945     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
141991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
141991     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''