TestLocalSymbols

2

tests

0

failures

0

ignored

4.933s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 4.905s passed
testSkolemization() 0.028s passed

Standard output

78179      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
78179      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
78179      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
78179      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
78179      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
78179      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
78179      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
78179      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
78179      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
78179      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
78179      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
78195      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
78195      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
78195      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
78233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
78233      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 444.3ns 
78233      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
78515      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
78515      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
78515      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
78515      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
79516      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
82559      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.32s 
82606      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
82668      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.4ns 
82731      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
82778      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
83044      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''