TestLocalSymbols

2

tests

0

failures

0

ignored

6.855s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 6.813s passed
testSkolemization() 0.042s passed

Standard output

111232     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
111232     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
111249     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
111250     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
111251     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
111251     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
111252     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
111254     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
111254     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
111254     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
111254     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
111254     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
111254     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
111254     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
111286     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
111301     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.08ms 
111301     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111754     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
111754     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
111770     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
111770     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
113584     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
117780     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.48s 
117858     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
117936     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 51.5ns 
117998     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
118045     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
118068     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''