TestLocalSymbols

2

tests

0

failures

0

ignored

4.588s

duration

100%

successful

Tests

Test Duration Result
testDoubleInstantiation() 4.551s passed
testSkolemization() 0.037s passed

Standard output

77494      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
77494      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
77510      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77510      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77510      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
77510      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77510      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77510      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule and_right 
77510      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
77510      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77510      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77510      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule or_right 
77525      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77525      DEBUG Test worker     d.u.i.k.p.m.ProofCorrectnessMgt No justification found for rule all_right 
77541      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Loading environment from src\test\resources\testcase\localSymbols\doubleSkolem.key 
77541      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Environment load took 426.2ns 
77541      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Creating init config 
77822      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
77822      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
77822      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
77822      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for Meta 
78822      DEBUG Test worker     d.u.i.k.j.TypeConverter   No LDT found for JavaBigintExpression 
81845      DEBUG Test worker     d.u.i.k.p.i.AbstractProblemLoader Init config took 4.28s 
81892      INFO  Test worker     d.u.i.k.p.i.AbstractProblemLoader Replaying proof doubleSkolem.key 
81939      DEBUG Test worker     d.u.i.k.p.i.IntermediateProofReplayer Proof replay took 33.4ns 
82016      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 1: 'rule orRight' 
82047      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 2: 'rule allRight formula='\forall int i; i > 0'' 
82060      DEBUG Test worker     d.u.i.k.m.s.ProofScriptEngine 3: 'rule allRight formula='\forall int i; i < 0''