TestLocalSymbols

2

tests

0

failures

0

ignored

9.352s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 9.274s passed
testSkolemization() 0.078s passed

Standard output

163323     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
163323     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
163323     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
163323     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
163323     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
163323     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
163323     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
163338     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
163338     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
163338     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
163338     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
163338     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
163338     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
163338     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
163385     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
163385     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 931.6ns 
163401     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
163932     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
163932     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
163932     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
163932     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
166152     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
172139     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 8.72s 
172249     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
172389     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 50.5ns 
172552     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 2, command: 'rule orRight' 
172599     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'' 
172614     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''