TestLocalSymbols

2

tests

0

failures

0

ignored

8.662s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 8.607s passed
testSkolemization() 0.055s passed

Standard output

132599     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
132599     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
132599     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
132599     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
132599     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
132599     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
132599     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
132614     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
132614     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
132614     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
132614     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
132614     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
132630     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
132630     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
132851     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
132851     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 589.6ns 
132866     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
133492     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
133492     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
133492     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
133492     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
135367     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
140745     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 7.83s 
140823     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
140917     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 41.7ns 
141163     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 2, command: 'rule orRight' 
141227     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'' 
141227     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''