TestLocalSymbols

2

tests

0

failures

0

ignored

4.406s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 4.374s passed
testSkolemization() 0.032s passed

Standard output

79127      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
79127      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
79127      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
79127      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
79127      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
79127      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
79127      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
79143      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
79143      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
79143      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
79143      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
79143      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
79143      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
79143      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
79158      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
79189      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 2.36ms 
79205      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
79486      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
79486      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
79486      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
79486      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
80314      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
83332      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.13s 
83378      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
83441      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.9ns 
83488      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
83519      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
83519      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''