TestLocalSymbols

2

tests

0

failures

0

ignored

5.218s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 5.167s passed
testSkolemization() 0.051s passed

Standard output

97841      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
97857      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
97857      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97857      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97857      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
97857      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97857      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97872      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
97872      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
97872      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97872      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97872      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
97872      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97872      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97950      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
97966      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.09ms 
97966      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98278      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
98294      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
98294      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
98294      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
99185      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
102828     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.86s 
102891     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
102953     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.1ns 
103000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
103047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
103047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''