TestLocalSymbols

2

tests

0

failures

0

ignored

7.015s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 6.968s passed
testSkolemization() 0.047s passed

Standard output

128672     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
128673     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
128677     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128678     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128678     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
128681     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128684     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128690     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
128691     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
128692     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128693     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128694     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
128694     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128695     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
128711     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/localSymbols/doubleSkolem.key 
128716     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 842.95ns 
128717     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
129124     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
129125     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
129127     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
129127     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
130768     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
135447     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.73s 
135496     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
135584     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.1ns 
135641     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine [1] goal: 0, source line: 2, command: 'rule orRight' 
135658     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'' 
135661     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''