TestLocalSymbols

2

tests

0

failures

0

ignored

5.914s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 5.867s passed
testSkolemization() 0.047s passed

Standard output

97718      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
97718      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
97718      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97718      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97718      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
97718      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97718      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97733      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
97733      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
97733      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97733      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97733      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
97733      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97733      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
97803      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
97834      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.81ms 
97850      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
98178      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
98178      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
98178      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
98178      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
99288      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
102943     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.1s 
103005     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
103068     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 45.8ns 
103165     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
103212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
103212     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''