TestLocalSymbols

2

tests

0

failures

0

ignored

8.685s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 8.629s passed
testSkolemization() 0.056s passed

Standard output

155011     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
155011     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
155027     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
155027     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
155027     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
155027     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
155027     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
155027     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
155027     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
155027     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
155027     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
155027     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
155043     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
155043     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
155074     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
155105     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 769.4ns 
155105     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
155652     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
155652     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
155652     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
155652     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
157511     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
163265     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.15s 
163358     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
163499     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 54.2ns 
163593     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
163671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
163671     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''