TestLocalSymbols

2

tests

0

failures

0

ignored

6.694s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 6.653s passed
testSkolemization() 0.041s passed

Standard output

131126     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
131127     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
131130     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
131131     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
131132     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
131133     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
131134     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
131140     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
131140     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
131141     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
131142     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
131142     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
131143     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
131144     DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
131161     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src/test/resources/testcase/localSymbols/doubleSkolem.key 
131168     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 1.04ms 
131169     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
131469     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
131470     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
131476     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
131476     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
132718     DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
137547     DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 6.38s 
137595     INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
137682     DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 36.3ns 
137758     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
137780     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
137788     DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''