TestLocalSymbols

2

tests

0

failures

0

ignored

5.813s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 5.779s passed
testSkolemization() 0.034s passed

Standard output

92242      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
92244      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
92246      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
92247      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
92248      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
92250      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
92252      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
92257      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
92257      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
92258      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
92259      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
92260      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
92261      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
92261      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
92274      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/localSymbols/doubleSkolem.key 
92278      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 903.8ns 
92279      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
92760      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
92760      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
92766      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
92766      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
94149      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
97826      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.55s 
97883      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
97925      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 37.8ns 
97995      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' on goal 0 (script from line 2) 
98027      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' on goal 1 (script from line 3) 
98033      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0'' on goal 2 (script from line 4)