TestLocalSymbols

2

tests

0

failures

0

ignored

6.914s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 6.864s passed
testSkolemization() 0.050s passed

Standard output

128627     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
128627     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
128627     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128627     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128627     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
128643     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128643     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128643     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
128643     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
128643     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128643     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128643     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
128643     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128643     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128677     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
128683     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 533.3ns 
128683     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129104     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
129104     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
129104     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
129104     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
130386     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
135184     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.47s 
135246     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
135356     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.9ns 
135465     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 2, command: 'rule orRight' 
135496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [2] goal: 1, source line: 3, command: 'rule allRight formula='\forall int i; i > 0'' 
135496     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [3] goal: 2, source line: 4, command: 'rule allRight formula='\forall int i; i < 0''