TestLocalSymbols

2

tests

0

failures

0

ignored

4.732s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 4.701s passed
testSkolemization() 0.031s passed

Standard output

77247      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
77247      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
77247      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77247      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77247      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
77247      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77263      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77268      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
77268      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
77269      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77270      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77270      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
77271      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77272      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77292      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
77292      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 390.7ns 
77307      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77526      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
77526      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
77526      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
77526      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
78276      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
81271      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 3.96s 
81334      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
81381      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.6ns 
81438      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
81844      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
81969      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''