TestLocalSymbols

2

tests

0

failures

0

ignored

6.782s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 6.727s passed
testSkolemization() 0.055s passed

Standard output

124257     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
124257     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
124257     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124257     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124257     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
124257     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124257     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124272     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
124272     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
124272     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124272     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124272     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
124272     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124272     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
124304     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
124313     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 832.4ns 
124318     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
124716     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
124717     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
124717     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
124718     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
125863     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
130646     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.33s 
130709     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
130826     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 44ns 
130943     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
130979     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
131010     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''