TestLocalSymbols

2

tests

0

failures

0

ignored

8.127s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 8.083s passed
testSkolemization() 0.044s passed

Standard output

123089     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
123089     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
123089     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
123089     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
123089     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
123089     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
123089     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
123105     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
123105     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
123105     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
123105     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
123105     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
123105     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
123105     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
123261     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
123261     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 862.8ns 
123277     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
123855     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
123855     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
123855     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
123855     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
125699     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
130735     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.37s 
130813     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
130922     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 62.1ns 
131000     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
131047     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
131173     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''