TestLocalSymbols

2

tests

0

failures

0

ignored

6.442s

duration

100%

successful

Tests

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

Standard output

83955      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
83955      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
83955      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83955      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83955      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
83955      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83971      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83971      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
83971      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
83971      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83971      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83971      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
83971      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
83971      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
84631      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
85632      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.2ms 
85632      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
85976      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
85976      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
85976      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
85976      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
86742      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
89806      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.17s 
89853      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
89899      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39ns 
89946      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
89978      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
90369      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''