TestLocalSymbols

2

tests

0

failures

0

ignored

6.360s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 6.316s passed
testSkolemization() 0.044s passed

Standard output

102317     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
102318     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
102323     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
102324     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
102324     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
102325     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
102326     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
102333     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
102333     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
102335     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
102335     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
102336     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
102337     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
102338     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
102351     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
102351     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 485ns 
102367     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
102790     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
102790     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
102790     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
102790     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
104228     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
108349     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.99s 
108427     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
108505     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 40ns 
108568     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
108630     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
108636     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''