TestLocalSymbols

2

tests

0

failures

0

ignored

7.204s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 7.144s passed
testSkolemization() 0.060s passed

Standard output

110887     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
110887     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
110887     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
110887     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
110887     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
110887     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
110887     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
110903     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
110903     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
110903     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
110903     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
110903     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
110903     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
110903     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
110959     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
110967     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 3.47ms 
110967     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
111373     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
111373     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
111389     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
111389     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
112986     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
117125     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.15s 
117203     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
117265     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 42.8ns 
117348     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
117420     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
117439     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''