TestLocalSymbols

2

tests

0

failures

0

ignored

5.061s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 5.027s passed
testSkolemization() 0.034s passed

Standard output

83206      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
83206      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
83206      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83206      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83206      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
83206      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83206      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83206      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
83206      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
83221      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83221      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83221      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
83221      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83221      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83237      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
83237      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 788.6ns 
83237      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
83534      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
83534      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
83534      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
83534      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
84785      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
88001      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.75s 
88048      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
88111      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40.8ns 
88189      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
88236      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
88242      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''