TestLocalSymbols

2

tests

0

failures

0

ignored

5.434s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 5.406s passed
testSkolemization() 0.028s passed

Standard output

89964      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
89965      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
89967      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
89967      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
89968      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
89968      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
89969      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
89973      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
89973      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
89974      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
89974      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
89975      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
89975      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
89976      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
89989      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/localSymbols/doubleSkolem.key 
89993      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.33ms 
89994      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
90321      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
90322      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
90324      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
90324      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
91701      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
95192      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 5.2s 
95237      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
95276      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 48.9ns 
95327      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
95369      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
95377      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''