TestLocalSymbols

2

tests

0

failures

0

ignored

7.474s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 7.417s passed
testSkolemization() 0.057s passed

Standard output

130792     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
130803     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
130807     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
130807     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
130808     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
130814     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
130815     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
130821     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
130822     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
130823     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
130824     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
130825     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
130826     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
130827     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
130852     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/localSymbols/doubleSkolem.key 
130858     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 983.1ns 
130859     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131325     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
131326     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
131327     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
131327     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
132808     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
137949     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.09s 
138019     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
138117     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 39ns 
138186     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
138223     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
138232     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''